1.1 --- a/test/Tools/isac/Test_Isac.thy	Sat Feb 10 16:21:12 2018 +0100
     1.2 +++ b/test/Tools/isac/Test_Isac.thy	Tue Feb 13 15:14:55 2018 +0100
     1.3 @@ -156,8 +156,6 @@
     1.4    ML {*"%%%%%%%%%%%%%%%%% end Minisubpbl.thy %%%%%%%%%%%%%%%%%%%%%%%";*}
     1.5    ML {*"%%%%%%%%%%%%%%%%% start Interpret.thy %%%%%%%%%%%%%%%%%%";*}
     1.6    ML_file "Interpret/mstools.sml"
     1.7 -
     1.8 -
     1.9    ML_file "Interpret/ctree.sml"         (*!...!see(25)*)
    1.10    ML_file "Interpret/ptyps.sml"         (* requires setup from ptyps.thy *)
    1.11    ML {* (*check_unsynchronized_ref (); ==== trick on error: CUT AND PASTE THIS LINE =========*) *}
    1.12 @@ -169,14 +167,6 @@
    1.13    ML_file "Interpret/appl.sml"          (*complete "WEGEN INTERMED TESTCODE"   *)
    1.14    ML_file "Interpret/rewtools.sml"
    1.15    ML_file "Interpret/script.sml"
    1.16 -
    1.17 -ML {*
    1.18 -"~~~~~ fun xxx, args:"; val () = ();
    1.19 -*} ML {*
    1.20 -*} ML {*
    1.21 -*}
    1.22 -
    1.23 -(*---------------------- check test file by testfile -------------------------------------------
    1.24    ML_file "Interpret/solve.sml"
    1.25    ML_file "Interpret/inform.sml"
    1.26  (*WITHOUT inhibit exn WN1130621 Isabelle2012-->13 !thehier! THIS ERROR OCCURS:
    1.27 @@ -205,6 +195,15 @@
    1.28    ML_file "Knowledge/atools.sml"
    1.29    ML_file "Knowledge/simplify.sml"
    1.30    ML_file "Knowledge/poly.sml"
    1.31 +
    1.32 +ML {*
    1.33 +"~~~~~ fun xxx, args:"; val () = ();
    1.34 +*} ML {*
    1.35 +
    1.36 +*} ML {*
    1.37 +*}
    1.38 +
    1.39 +(*---------------------- check test file by testfile -------------------------------------------
    1.40    ML_file "Knowledge/gcd_poly_ml.sml"
    1.41    ML_file "Knowledge/gcd_poly_winkler.sml" (*must be after gcd_poly_ml.sml: redefines functions*)
    1.42    ML_file "Knowledge/rational.sml"