1.1 --- a/src/Tools/isac/Knowledge/Test.thy	Wed Aug 03 13:22:36 2022 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Test.thy	Wed Aug 03 17:18:47 2022 +0200
     1.3 @@ -589,12 +589,11 @@
     1.4       (matches (?a+v_v = 0) e_e) | (matches (?a+?b*v_v = 0) e_e)"
     1.5    Find: "solutions v_v'i'"
     1.6  
     1.7 +setup \<open>KEStore_Elems.add_rew_ord [
     1.8 +  ("termlessI", termlessI),
     1.9 +  ("ord_make_polytest", ord_make_polytest false \<^theory>)]\<close>
    1.10 +
    1.11  ML \<open>
    1.12 -Rewrite_Ord.rew_ord' := overwritel (! Rewrite_Ord.rew_ord',
    1.13 -[("termlessI", termlessI),
    1.14 - ("ord_make_polytest", ord_make_polytest false \<^theory>)
    1.15 - ]);
    1.16 -
    1.17  val make_polytest =
    1.18    Rule_Def.Repeat{id = "make_polytest", preconds = []:term list, 
    1.19      rew_ord = ("ord_make_polytest", ord_make_polytest false @{theory "Poly"}),