1.1 --- a/test/Tools/isac/Knowledge/algein.sml	Mon Oct 31 18:28:36 2022 +0100
     1.2 +++ b/test/Tools/isac/Knowledge/algein.sml	Mon Nov 07 17:37:20 2022 +0100
     1.3 @@ -100,10 +100,10 @@
     1.4  val thy = @{theory "Isac_Knowledge"}; 
     1.5  val ctxt = Proof_Context.init_global thy;
     1.6  val rew_ord = Rewrite_Ord.function_empty;
     1.7 -val erls = Rule_Set.Empty;
     1.8 +val asm_rls = Rule_Set.Empty;
     1.9  val thm = ThmC.thm_from_thy thy "sym_mult_zero_right";
    1.10  val t = TermC.parse_test @{context} "0 = (0::real)";
    1.11 -val SOME (t',_) = rewrite_ ctxt rew_ord erls false thm t;
    1.12 +val SOME (t',_) = rewrite_ ctxt rew_ord asm_rls false thm t;
    1.13  UnparseC.term t' = "0 = ?a1 * 0"; (* = true*)
    1.14  
    1.15  val sube = ["?a1 = (3::real)"];
    1.16 @@ -119,6 +119,6 @@
    1.17  
    1.18  val thm = ThmC.thm_from_thy thy "sym";
    1.19  (*----- STOPPED.WN0x?: Widerspruch 3 = 777: sym contains "==>" instead of "=" !!!
    1.20 -val SOME (t''',_) = rewrite_ thy rew_ord erls false thm t'';
    1.21 +val SOME (t''',_) = rewrite_ thy rew_ord asm_rls false thm t'';
    1.22  *)
    1.23  ( *----------------^^^^^^^^^^^^^^ ERROR Unbound schematic variable: ?a1*)