1.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy	Sat Jul 17 14:05:28 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy	Sun Jul 18 16:20:32 2021 +0200
     1.3 @@ -67,7 +67,7 @@
     1.4      end;
     1.5  
     1.6  (*("occur_exactly_in", ("EqSystem.occur_exactly_in", 
     1.7 -			eval_occur_exactly_in "#eval_occur_exactly_in_"))*)
     1.8 +                        eval_occur_exactly_in "#eval_occur_exactly_in_") )*)
     1.9  fun eval_occur_exactly_in _ "EqSystem.occur_exactly_in"
    1.10  			  (p as (Const ("EqSystem.occur_exactly_in",_) 
    1.11  				       $ vs $ all $ t)) _ =
    1.12 @@ -346,7 +346,9 @@
    1.13  		     erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
    1.14  		     rules = [(*for precond NTH_CONS ...*)
    1.15  			      Rule.Eval ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
    1.16 -			      Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_")
    1.17 +			      Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
    1.18 +            Rule.Eval ("EqSystem.occur_exactly_in", 
    1.19 +              eval_occur_exactly_in "#eval_occur_exactly_in_")
    1.20  			      (*immediately repeated rewrite pushes
    1.21  					    '+' into precondition !*)
    1.22  			      ],