diff -r 0c10aeff57d7 -r e5e9a6c45597 src/Tools/isac/Knowledge/EqSystem.thy
--- a/src/Tools/isac/Knowledge/EqSystem.thy	Sat Jul 17 14:05:28 2021 +0200
+++ b/src/Tools/isac/Knowledge/EqSystem.thy	Sun Jul 18 16:20:32 2021 +0200
@@ -67,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)) _ =
@@ -346,7 +346,9 @@
 		     erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
 		     rules = [(*for precond NTH_CONS ...*)
 			      Rule.Eval ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
-			      Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_")
+			      Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
+            Rule.Eval ("EqSystem.occur_exactly_in", 
+              eval_occur_exactly_in "#eval_occur_exactly_in_")
 			      (*immediately repeated rewrite pushes
 					    '+' into precondition !*)
 			      ],