1.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy	Mon Jun 21 22:08:01 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy	Sun Jul 18 18:15:27 2021 +0200
     1.3 @@ -49,6 +49,8 @@
     1.4      works for lists of any length, interestingly !?!*)
     1.5  
     1.6  ML \<open>
     1.7 +val thy = @{theory};
     1.8 +
     1.9  (** eval functions **)
    1.10  
    1.11  (*certain variables of a given list occur _all_ in a term
    1.12 @@ -65,7 +67,7 @@
    1.13      end;
    1.14  
    1.15  (*("occur_exactly_in", ("EqSystem.occur_exactly_in", 
    1.16 -			eval_occur_exactly_in "#eval_occur_exactly_in_"))*)
    1.17 +                        eval_occur_exactly_in "#eval_occur_exactly_in_") )*)
    1.18  fun eval_occur_exactly_in _ "EqSystem.occur_exactly_in"
    1.19  			  (p as (Const ("EqSystem.occur_exactly_in",_) 
    1.20  				       $ vs $ all $ t)) _ =
    1.21 @@ -153,8 +155,8 @@
    1.22      (term_ord' pr thy (Library.swap tu) = LESS);*)
    1.23  
    1.24  (*for the rls's*)
    1.25 -fun ord_simplify_System (pr:bool) thy _(*subst*) tu = 
    1.26 -    (term_ord' pr thy tu = LESS);
    1.27 +fun ord_simplify_System (pr:bool) thy _(*subst*) (ts, us) = 
    1.28 +    (term_ord' pr thy (TermC.numerals_to_Free ts, TermC.numerals_to_Free us) = LESS);
    1.29  (**)
    1.30  end;
    1.31  (**)
    1.32 @@ -336,7 +338,9 @@
    1.33  		     erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
    1.34  		     rules = [(*for precond NTH_CONS ...*)
    1.35  			      \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
    1.36 -			      \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")
    1.37 +			      \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
    1.38 +            Rule.Eval ("EqSystem.occur_exactly_in", 
    1.39 +              eval_occur_exactly_in "#eval_occur_exactly_in_")
    1.40  			      (*immediately repeated rewrite pushes
    1.41  					    '+' into precondition !*)
    1.42  			      ],