diff -r ce09935439b3 -r 2e0b7ca391dc src/Tools/isac/BaseDefinitions/rewrite-order.sml
--- a/src/Tools/isac/BaseDefinitions/rewrite-order.sml	Wed Aug 03 18:17:27 2022 +0200
+++ b/src/Tools/isac/BaseDefinitions/rewrite-order.sml	Thu Aug 04 12:48:37 2022 +0200
@@ -4,16 +4,17 @@
 *)
 signature REWRITE_ORDER =
 sig
-  val e_rew_ord': Rule_Def.rew_ord';
-  val dummy_ord: Rule_Def.rew_ord_
-  val e_rew_ord: Rule_Def.rew_ord_
+  type id = Rule_Def.rew_ord_id
+  val id_empty: id
 
-  type rew_ord = Rule_Def.rew_ord
-  val e_rew_ordX: rew_ord
-  val to_string: rew_ord -> string
+  type function = Rule_Def.rew_ord_function
+  val function_empty: function
 
-  type rew_ord' = Rule_Def.rew_ord'
-  val equal: rew_ord * rew_ord -> bool
+  type T = Rule_Def.rew_ord_T
+  val empty: T
+
+  val to_string: T -> string
+  val equal: T * T -> bool
 end
 
 (**)
@@ -21,17 +22,16 @@
 struct
 (**)
 
-val e_rew_ord' = "e_rew_ord" : Rule_Def.rew_ord';
-type rew_ord_ = Rule_Def.rew_ord_;
-fun dummy_ord (_: subst) (_: term, _: term) = true;
-val e_rew_ord_ = dummy_ord;
+type id = Rule_Def.rew_ord_id
+val id_empty = "Rewrite_Ord.id_empty";
 
-type rew_ord = (*rew_ord' * rew_ord_;*) Rule_Def.rew_ord
-val e_rew_ord = dummy_ord; (* TODO.WN071231 clarify identifiers..e_rew_ordX*)
-val e_rew_ordX = (e_rew_ord', e_rew_ord_)
+type function = Rule_Def.rew_ord_function;
+fun function_empty (_: LibraryC.subst) (_: term, _: term) = true;
+
+type T = Rule_Def.rew_ord_T
+val empty = (id_empty, function_empty)
+
 fun to_string (rew_ord', _) = "(" ^ rew_ord' ^ ", _: fn)"
-
-type rew_ord' = Rule_Def.rew_ord'
 fun equal ((id1, _), (id2, _)) = id1 = id2
 
 end