1.1 --- a/src/Tools/isac/Knowledge/Base_Tools.thy	Wed Apr 08 15:50:03 2020 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Base_Tools.thy	Wed Apr 08 16:56:47 2020 +0200
     1.3 @@ -46,12 +46,12 @@
     1.4    fun term_ordI (_: Rule.subst) uv = Term_Ord.term_ord uv;
     1.5  end;
     1.6  \<close> ML \<open>
     1.7 -(*TODO.WN0509 reduce ids: tless_true = e_rew_ord' = Rule.e_rew_ord = Rule.dummy_ord*)
     1.8 -val tless_true = Rule.dummy_ord;
     1.9 -Rule.rew_ord' := overwritel (! Rule.rew_ord', (*<<<---- use KEStore.xxx here, too*)
    1.10 +(*TODO.WN0509 reduce ids: tless_true = e_rew_ord' = Rewrite_Ord.e_rew_ord = Rewrite_Ord.dummy_ord*)
    1.11 +val tless_true = Rewrite_Ord.dummy_ord;
    1.12 +Rewrite_Ord.rew_ord' := overwritel (! Rewrite_Ord.rew_ord', (*<<<---- use KEStore.xxx here, too*)
    1.13  			[("tless_true", tless_true),
    1.14  			 ("e_rew_ord'", tless_true),
    1.15 -			 ("dummy_ord", Rule.dummy_ord)]);
    1.16 +			 ("dummy_ord", Rewrite_Ord.dummy_ord)]);
    1.17  \<close>
    1.18  
    1.19  subsection \<open>rule-sets\<close>