1.1 --- a/src/Tools/isac/BaseDefinitions/rewrite-order.sml	Tue Jun 21 13:51:04 2022 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/rewrite-order.sml	Tue Jun 21 16:04:43 2022 +0200
     1.3 @@ -4,7 +4,6 @@
     1.4  *)
     1.5  signature REWRITE_ORDER =
     1.6  sig
     1.7 -  type subst
     1.8    val e_rew_ord': Rule_Def.rew_ord';
     1.9    val dummy_ord: Rule_Def.rew_ord_
    1.10    val e_rew_ord: Rule_Def.rew_ord_
    1.11 @@ -14,8 +13,8 @@
    1.12    val to_string: rew_ord -> string
    1.13  
    1.14    type rew_ord' = Rule_Def.rew_ord'
    1.15 -  val rew_ord': (rew_ord' * (subst -> term * term -> bool)) list Unsynchronized.ref
    1.16 -  val assoc_rew_ord: string -> subst -> term * term -> bool
    1.17 +  val rew_ord': (rew_ord' * (LibraryC.subst -> term * term -> bool)) list Unsynchronized.ref
    1.18 +  val assoc_rew_ord: string -> LibraryC.subst -> term * term -> bool
    1.19  end
    1.20  
    1.21  (**)
    1.22 @@ -25,7 +24,6 @@
    1.23  
    1.24  val e_rew_ord' = "e_rew_ord" : Rule_Def.rew_ord';
    1.25  type rew_ord_ = Rule_Def.rew_ord_;
    1.26 -type subst = (term * term) list;
    1.27  fun dummy_ord (_: subst) (_: term, _: term) = true;
    1.28  val e_rew_ord_ = dummy_ord;
    1.29