test/Tools/isac/Test_Isac_Short.thy
changeset 60608 5dabcc1c9235
parent 60603 eec3b6fd6c7a
child 60610 798e54862b08
     1.1 --- a/test/Tools/isac/Test_Isac_Short.thy	Sat Dec 03 19:12:38 2022 +0100
     1.2 +++ b/test/Tools/isac/Test_Isac_Short.thy	Sun Dec 04 16:48:06 2022 +0100
     1.3 @@ -132,7 +132,10 @@
     1.4    open ThmC_Def
     1.5    open ThmC
     1.6    open Rewrite_Ord
     1.7 -  open UnparseC
     1.8 +  open UnparseC;
     1.9 +
    1.10 +  Know_Store.set_ref_last_thy @{theory};
    1.11 +  (*otherwise ERRORs in pbl-met-hierarchy.sml, refine.sml, evaluate.sml*)
    1.12  \<close>
    1.13  
    1.14  ML \<open>
    1.15 @@ -185,7 +188,6 @@
    1.16  \<close>
    1.17  
    1.18  ML \<open>
    1.19 -  Know_Store.set_ref_thy @{theory};
    1.20    (*fun autoCalculate' cI auto = autoCalculate cI auto (*|> Future.join*)*);
    1.21  \<close>
    1.22