1.1 --- a/test/Tools/isac/Knowledge/algein.sml	Sat Apr 04 12:11:32 2020 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/algein.sml	Mon Apr 06 11:44:36 2020 +0200
     1.3 @@ -102,7 +102,7 @@
     1.4  "----------- Widerspruch 3 = 777 ---------------------------------";
     1.5  val thy = @{theory "Isac_Knowledge"}; 
     1.6  val rew_ord = dummy_ord;
     1.7 -val erls = Erls;
     1.8 +val erls = Rule_Set.Empty;
     1.9  val thm = assoc_thm' thy ("sym_mult_zero_right","");
    1.10  val t = str2term "0 = (0::real)";
    1.11  val SOME (t',_) = rewrite_ thy rew_ord erls false thm t;