1.1 --- a/test/Tools/isac/Test_Isac.thy	Mon Mar 26 14:20:57 2018 +0200
     1.2 +++ b/test/Tools/isac/Test_Isac.thy	Mon Mar 26 16:25:01 2018 +0200
     1.3 @@ -169,18 +169,13 @@
     1.4    ML_file "Interpret/ctree.sml"         (*!...!see(25)*)
     1.5    ML_file "Interpret/ptyps.sml"         (* requires setup from ptyps.thy *)
     1.6    ML {* (*check_unsynchronized_ref (); ==== trick on error: CUT AND PASTE THIS LINE =========*) *}
     1.7 -(*TRICK DOESN'T WORK: get_pbt not found: ["IsacKnowledge","Diff","Theorems","diff_sin_chain"]*)
     1.8    ML_file "Interpret/generate.sml"
     1.9 -(*WITHOUT inhibit exn WN1130621 Isabelle2012-->13 !thehier! THIS ERROR OCCURS:
    1.10 -  ... SAME ERROR HERE ON ISABELLE2012 AS IN ISAC ON ISABELLE2011*)
    1.11    ML_file "Interpret/calchead.sml"
    1.12    ML_file "Interpret/appl.sml"          (*complete "WEGEN INTERMED TESTCODE"   *)
    1.13    ML_file "Interpret/rewtools.sml"
    1.14    ML_file "Interpret/script.sml"
    1.15    ML_file "Interpret/solve.sml"
    1.16    ML_file "Interpret/inform.sml"
    1.17 -(*WITHOUT inhibit exn WN1130621 Isabelle2012-->13 !thehier! THIS ERROR OCCURS:
    1.18 -  ... SAME ERROR HERE ON ISABELLE2012 AS IN ISAC ON ISABELLE2011*)
    1.19    ML_file "Interpret/mathengine.sml"    (*!part. WN130804: +check Interpret/me.sml*)
    1.20    ML {*"%%%%%%%%%%%%%%%%% end Interpret.thy %%%%%%%%%%%%%%%%%%%%";*}
    1.21    ML {*"%%%%%%%%%%%%%%%%% start xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%";*}