1.1 --- a/test/Tools/isac/Interpret/rewtools.sml	Wed Oct 06 14:52:12 2010 +0200
     1.2 +++ b/test/Tools/isac/Interpret/rewtools.sml	Wed Oct 06 15:12:41 2010 +0200
     1.3 @@ -442,7 +442,7 @@
     1.4  "----- these work ?!?";
     1.5  val th = sym_thm real_minus_eq_cancel;
     1.6  val Th = sym_Thm (Thm ("real_minus_eq_cancel", real_minus_eq_cancel));
     1.7 -val th'= mk_thm Isac.thy ((de_quote o string_of_thm) real_minus_eq_cancel);
     1.8 +val th'= mk_thm (theory "Isac") ((de_quote o string_of_thm) real_minus_eq_cancel);
     1.9  val th'= mk_thm Biegelinie.thy((de_quote o string_of_thm)real_minus_eq_cancel);
    1.10  
    1.11  "----- DIFFERENCE TO ABOVE ?!?: this is still ok, when called in next_tac...";
    1.12 @@ -504,7 +504,7 @@
    1.13  "----------- fun filter_appl_rews --------------------------------";
    1.14  "----------- fun filter_appl_rews --------------------------------";
    1.15  val f = str2term "a + z + 2*a + 3*z + 5 + 6";
    1.16 -val thy = assoc_thy "Isac.thy";
    1.17 +val thy = assoc_thy "Isac";
    1.18  val subst = [(*TODO.WN071231 test Rewrite_Inst*)];
    1.19  val rls = Test_simplify;
    1.20  (* val rls = rls_p_33;      filter_appl_rews  ---> length 2