src/Tools/isac/BaseDefinitions/rewrite-order.sml
changeset 60436 1c8263e775d4
parent 60264 b987b05f1ca8
child 60477 4ac966aaa785
     1.1 --- a/src/Tools/isac/BaseDefinitions/rewrite-order.sml	Sun May 29 19:05:14 2022 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/rewrite-order.sml	Tue May 31 09:16:12 2022 +0200
     1.3 @@ -1,8 +1,6 @@
     1.4  (* Title:  BaseDefinitions/rewrite-order.sml
     1.5     Author: Walther Neuper
     1.6     (c) due to copyright terms
     1.7 -
     1.8 -TODO: use "Rewrite_Ord" for renaming identifiers.
     1.9  *)
    1.10  signature REWRITE_ORDER =
    1.11  sig
    1.12 @@ -13,6 +11,7 @@
    1.13  
    1.14    type rew_ord = Rule_Def.rew_ord
    1.15    val e_rew_ordX: rew_ord
    1.16 +  val to_string: rew_ord -> string
    1.17  
    1.18    type rew_ord' = Rule_Def.rew_ord'
    1.19    val rew_ord': (rew_ord' * (subst -> term * term -> bool)) list Unsynchronized.ref
    1.20 @@ -33,6 +32,7 @@
    1.21  type rew_ord = (*rew_ord' * rew_ord_;*) Rule_Def.rew_ord
    1.22  val e_rew_ord = dummy_ord; (* TODO.WN071231 clarify identifiers..e_rew_ordX*)
    1.23  val e_rew_ordX = (e_rew_ord', e_rew_ord_)
    1.24 +fun to_string (rew_ord', _) = "(" ^ rew_ord' ^ ", _: fn)"
    1.25  
    1.26  type rew_ord' = Rule_Def.rew_ord'
    1.27  (* rewrite orders, also stored in 'type met' and type 'and rls'