1.1 --- a/src/Tools/isac/BaseDefinitions/rewrite-order.sml	Wed Aug 03 17:18:47 2022 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/rewrite-order.sml	Wed Aug 03 18:06:02 2022 +0200
     1.3 @@ -32,16 +32,6 @@
     1.4  fun to_string (rew_ord', _) = "(" ^ rew_ord' ^ ", _: fn)"
     1.5  
     1.6  type rew_ord' = Rule_Def.rew_ord'
     1.7 -(* rewrite orders, also stored in 'type met' and type 'and rls'
     1.8 -  The association list is required for 'rewrite.."rew_ord"..' *)
     1.9 -val rew_ord' = Unsynchronized.ref
    1.10 -  ([("e_rew_ord", e_rew_ord), ("dummy_ord", dummy_ord)]
    1.11 -	: (rew_ord' *    (* the key for the association list         *)
    1.12 -	    (subst 	    (* the bound variables - they get high order*)
    1.13 -	     -> (term * term) (* (t1, t2) to be compared                  *)
    1.14 -	     -> bool))        (* if t1 <= t2 then true else false         *)
    1.15 -		list);              (* association list                         *)
    1.16 -
    1.17  fun equal ((id1, _), (id2, _)) = id1 = id2
    1.18  
    1.19  end