diff -r b7071d1dd263 -r 007ef64dbb08 test/Tools/isac/Knowledge/algein.sml
--- a/test/Tools/isac/Knowledge/algein.sml	Mon Oct 31 18:28:36 2022 +0100
+++ b/test/Tools/isac/Knowledge/algein.sml	Mon Nov 07 17:37:20 2022 +0100
@@ -100,10 +100,10 @@
 val thy = @{theory "Isac_Knowledge"}; 
 val ctxt = Proof_Context.init_global thy;
 val rew_ord = Rewrite_Ord.function_empty;
-val erls = Rule_Set.Empty;
+val asm_rls = Rule_Set.Empty;
 val thm = ThmC.thm_from_thy thy "sym_mult_zero_right";
 val t = TermC.parse_test @{context} "0 = (0::real)";
-val SOME (t',_) = rewrite_ ctxt rew_ord erls false thm t;
+val SOME (t',_) = rewrite_ ctxt rew_ord asm_rls false thm t;
 UnparseC.term t' = "0 = ?a1 * 0"; (* = true*)
 
 val sube = ["?a1 = (3::real)"];
@@ -119,6 +119,6 @@
 
 val thm = ThmC.thm_from_thy thy "sym";
 (*----- STOPPED.WN0x?: Widerspruch 3 = 777: sym contains "==>" instead of "=" !!!
-val SOME (t''',_) = rewrite_ thy rew_ord erls false thm t'';
+val SOME (t''',_) = rewrite_ thy rew_ord asm_rls false thm t'';
 *)
 ( *----------------^^^^^^^^^^^^^^ ERROR Unbound schematic variable: ?a1*)