1.1 --- a/src/Tools/isac/Knowledge/Base_Tools.thy	Sun Apr 19 11:07:02 2020 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Base_Tools.thy	Sun Apr 19 12:22:37 2020 +0200
     1.3 @@ -48,7 +48,7 @@
     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 KEStore.xxx here, too*)
     1.8 +Rewrite_Ord.rew_ord' := overwritel (! Rewrite_Ord.rew_ord', (*<<<---- use Know_Store.xxx here, too*)
     1.9  			[("tless_true", tless_true),
    1.10  			 ("e_rew_ord'", tless_true),
    1.11  			 ("dummy_ord", Rewrite_Ord.dummy_ord)]);