[isabelle] Strange errors after processing theory file



I am having a strange event when importing a theory. It processes  
fine, then there seems to be some problem with registering it as  
processed, namely ~2000 lines a MATCH warnings/errors. A partial trace  
from a ProofGeneral session follows, but it does not appear to be  
ProofGeneral specific as the warnings turn up in a build log as well.

\<^sync>ProofGeneral.inform_file_processed "/home/mahonyb/work/ver/REP/ 
HiVe_Isa08/mathKit/Equipotence.thy"; \<^sync>;
Enter MATCH
%a b c d e. e =?= ?P48 z
%a b. b =?= ?P23 z
%a b c. c =?= ?P22 z
%a b c. c =?= ?P21 z
%a b c. c =?= ?P20 z
%a b c. c =?= ?P19 z
%a b. b =?= ?P18 z
%a b. b =?= ?P17 z
%a b c. c =?= ?P16 z
%a b c. c =?= ?P15 z
%a b c. c =?= ?P14 z
%a b c. c =?= ?P13 z
%a b. b =?= ?P12 z
%a. a =?= ?P11 z
%a b c. c =?= ?P10 z
%a b c. c =?= ?P9 z
%a b c. c =?= ?P8 z
%a b c. c =?= ?P7 z
%a b. b =?= ?P6 z
%a. a =?= ?P5 z
Enter MATCH

etc etc etc


IMPORTANT: This email remains the property of the Australian Defence Organisation and is subject to the jurisdiction of section 70 of the CRIMES ACT 1914.  If you have received this email in error, you are requested to contact the sender and delete the email.







This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.