src/Tools/isac/BaseDefinitions/rewrite-order.sml
changeset 60506 145e45cd7a0f
parent 60477 4ac966aaa785
child 60507 b125dcf14489
     1.1 --- a/src/Tools/isac/BaseDefinitions/rewrite-order.sml	Wed Aug 03 13:22:36 2022 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/rewrite-order.sml	Wed Aug 03 17:18:47 2022 +0200
     1.3 @@ -13,8 +13,7 @@
     1.4    val to_string: rew_ord -> string
     1.5  
     1.6    type rew_ord' = Rule_Def.rew_ord'
     1.7 -  val rew_ord': (rew_ord' * (LibraryC.subst -> term * term -> bool)) list Unsynchronized.ref
     1.8 -  val assoc_rew_ord: string -> LibraryC.subst -> term * term -> bool
     1.9 +  val equal: rew_ord * rew_ord -> bool
    1.10  end
    1.11  
    1.12  (**)
    1.13 @@ -42,10 +41,7 @@
    1.14  	     -> (term * term) (* (t1, t2) to be compared                  *)
    1.15  	     -> bool))        (* if t1 <= t2 then true else false         *)
    1.16  		list);              (* association list                         *)
    1.17 -fun assoc' ([], key) = raise ERROR ("ME_Isa: \"" ^ key ^ "\" not known")
    1.18 -  | assoc' ((keyi, xi) :: pairs, key) =
    1.19 -    if key = keyi then SOME xi else assoc' (pairs, key);
    1.20 -fun assoc_rew_ord ro = ((the o assoc') (! rew_ord', ro))
    1.21 -  handle ERROR _ => raise ERROR ("ME_Isa: rew_ord '" ^ ro ^ "' not in system");
    1.22  
    1.23 -end
    1.24 \ No newline at end of file
    1.25 +fun equal ((id1, _), (id2, _)) = id1 = id2
    1.26 +
    1.27 +end