1.1 --- a/test/Tools/isac/Knowledge/algein.sml	Mon Apr 13 18:37:24 2020 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/algein.sml	Tue Apr 14 12:39:26 2020 +0200
     1.3 @@ -103,7 +103,7 @@
     1.4  val thy = @{theory "Isac_Knowledge"}; 
     1.5  val rew_ord = dummy_ord;
     1.6  val erls = Rule_Set.Empty;
     1.7 -val thm = assoc_thm' thy ("sym_mult_zero_right","");
     1.8 +val thm = assoc_thm'' thy "sym_mult_zero_right";
     1.9  val t = str2term "0 = (0::real)";
    1.10  val SOME (t',_) = rewrite_ thy rew_ord erls false thm t;
    1.11  UnparseC.term t' = "0 = ?a1 * 0"; (* = true*)
    1.12 @@ -118,7 +118,7 @@
    1.13  val t'' = subst_atomic subst t';
    1.14  UnparseC.term t'' = "0 = 3 * 0"; (* = true*)
    1.15  
    1.16 -val thm = assoc_thm' thy ("sym","");
    1.17 +val thm = assoc_thm'' thy "sym";
    1.18  (*----- STOPPED.WN0x?: Widerspruch 3 = 777: sym contains "==>" instead of "=" !!!
    1.19  val SOME (t''',_) = rewrite_ thy rew_ord erls false thm t'';
    1.20  *)