1.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy	Wed Aug 03 13:22:36 2022 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy	Wed Aug 03 17:18:47 2022 +0200
     1.3 @@ -159,13 +159,13 @@
     1.4  (*for the rls's*)
     1.5  fun ord_simplify_System (pr:bool) thy _(*subst*) (ts, us) = 
     1.6      (term_ord' pr thy (TermC.numerals_to_Free ts, TermC.numerals_to_Free us) = LESS);
     1.7 -(**)
     1.8 -end;
     1.9 -(**)
    1.10 -Rewrite_Ord.rew_ord' := overwritel (! Rewrite_Ord.rew_ord',
    1.11 -[("ord_simplify_System", ord_simplify_System false \<^theory>)
    1.12 - ]);
    1.13 +
    1.14 +(**)end;(**)
    1.15 +\<close> ML \<open>
    1.16  \<close>
    1.17 +setup \<open>KEStore_Elems.add_rew_ord [
    1.18 +  ("ord_simplify_System", ord_simplify_System false \<^theory>)]\<close>
    1.19 +
    1.20  ML \<open>
    1.21  (** rulesets **)
    1.22