diff -r ce09935439b3 -r 2e0b7ca391dc src/Tools/isac/Knowledge/Base_Tools.thy
--- a/src/Tools/isac/Knowledge/Base_Tools.thy	Wed Aug 03 18:17:27 2022 +0200
+++ b/src/Tools/isac/Knowledge/Base_Tools.thy	Thu Aug 04 12:48:37 2022 +0200
@@ -50,15 +50,15 @@
   fun term_ordI (_: subst) uv = Term_Ord.term_ord uv;
 end;
 \<close> ML \<open>
-(*TODO.WN0509 reduce ids: tless_true = e_rew_ord' = Rewrite_Ord.e_rew_ord = Rewrite_Ord.dummy_ord*)
-val tless_true = Rewrite_Ord.dummy_ord;
+(*TODO.WN0509 reduce ids: tless_true = e_rew_ord' = Rewrite_Ord.function_empty = Rewrite_Ord.function_empty*)
+val tless_true = Rewrite_Ord.function_empty;
 \<close> ML \<open>
 \<close> 
 setup \<open>KEStore_Elems.add_rew_ord [
   ("tless_true", tless_true),
-	("e_rew_ord", tless_true),
+	("Rewrite_Ord.id_empty", tless_true),
 	("e_rew_ord'", tless_true),
-	("dummy_ord", Rewrite_Ord.dummy_ord)]\<close>
+	("dummy_ord", Rewrite_Ord.function_empty)]\<close>
 
 subsection \<open>rule-sets\<close>
 ML \<open>