1.1 --- a/src/Tools/isac/Knowledge/Poly.thy	Wed Aug 03 13:22:36 2022 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Poly.thy	Wed Aug 03 17:18:47 2022 +0200
     1.3 @@ -549,10 +549,10 @@
     1.4      (term_ord' pr thy(***) (TermC.numerals_to_Free ts, TermC.numerals_to_Free us) = LESS );
     1.5  
     1.6  end;(*local*)
     1.7 -
     1.8 -Rewrite_Ord.rew_ord' := overwritel (! Rewrite_Ord.rew_ord', (* TODO: make analogous to KEStore_Elems.add_mets *)
     1.9 -[("termlessI", termlessI), ("ord_make_polynomial", ord_make_polynomial false \<^theory>)]);
    1.10 -\<close>
    1.11 +\<close> 
    1.12 +setup \<open>KEStore_Elems.add_rew_ord [
    1.13 +  ("termlessI", termlessI), 
    1.14 +  ("ord_make_polynomial", ord_make_polynomial false \<^theory>)]\<close>
    1.15  
    1.16  subsection \<open>predicates\<close>
    1.17  subsubsection \<open>in specifications\<close>