diff -r 63cecf440235 -r 40eb8aa2b0d6 src/Tools/isac/Knowledge/EqSystem.thy
--- a/src/Tools/isac/Knowledge/EqSystem.thy	Mon Jun 21 22:08:01 2021 +0200
+++ b/src/Tools/isac/Knowledge/EqSystem.thy	Sun Jul 18 18:15:27 2021 +0200
@@ -49,6 +49,8 @@
     works for lists of any length, interestingly !?!*)
 
 ML \<open>
+val thy = @{theory};
+
 (** eval functions **)
 
 (*certain variables of a given list occur _all_ in a term
@@ -65,7 +67,7 @@
     end;
 
 (*("occur_exactly_in", ("EqSystem.occur_exactly_in", 
-			eval_occur_exactly_in "#eval_occur_exactly_in_"))*)
+                        eval_occur_exactly_in "#eval_occur_exactly_in_") )*)
 fun eval_occur_exactly_in _ "EqSystem.occur_exactly_in"
 			  (p as (Const ("EqSystem.occur_exactly_in",_) 
 				       $ vs $ all $ t)) _ =
@@ -153,8 +155,8 @@
     (term_ord' pr thy (Library.swap tu) = LESS);*)
 
 (*for the rls's*)
-fun ord_simplify_System (pr:bool) thy _(*subst*) tu = 
-    (term_ord' pr thy tu = LESS);
+fun ord_simplify_System (pr:bool) thy _(*subst*) (ts, us) = 
+    (term_ord' pr thy (TermC.numerals_to_Free ts, TermC.numerals_to_Free us) = LESS);
 (**)
 end;
 (**)
@@ -336,7 +338,9 @@
 		     erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
 		     rules = [(*for precond NTH_CONS ...*)
 			      \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
-			      \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")
+			      \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
+            Rule.Eval ("EqSystem.occur_exactly_in", 
+              eval_occur_exactly_in "#eval_occur_exactly_in_")
 			      (*immediately repeated rewrite pushes
 					    '+' into precondition !*)
 			      ],