1.1 --- a/src/Tools/isac/Knowledge/Base_Tools.thy	Wed Aug 03 13:22:36 2022 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Base_Tools.thy	Wed Aug 03 17:18:47 2022 +0200
     1.3 @@ -52,11 +52,13 @@
     1.4  \<close> ML \<open>
     1.5  (*TODO.WN0509 reduce ids: tless_true = e_rew_ord' = Rewrite_Ord.e_rew_ord = Rewrite_Ord.dummy_ord*)
     1.6  val tless_true = Rewrite_Ord.dummy_ord;
     1.7 -Rewrite_Ord.rew_ord' := overwritel (! Rewrite_Ord.rew_ord', (*<<<---- use Know_Store.xxx here, too*)
     1.8 -			[("tless_true", tless_true),
     1.9 -			 ("e_rew_ord'", tless_true),
    1.10 -			 ("dummy_ord", Rewrite_Ord.dummy_ord)]);
    1.11 -\<close>
    1.12 +\<close> ML \<open>
    1.13 +\<close> 
    1.14 +setup \<open>KEStore_Elems.add_rew_ord [
    1.15 +  ("tless_true", tless_true),
    1.16 +	("e_rew_ord", tless_true),
    1.17 +	("e_rew_ord'", tless_true),
    1.18 +	("dummy_ord", Rewrite_Ord.dummy_ord)]\<close>
    1.19  
    1.20  subsection \<open>rule-sets\<close>
    1.21  ML \<open>