# HG changeset patch # User wenzelm # Date 1144922450 -7200 # Node ID a21431e996bfff0595279034356da80b5f90c328 # Parent f753592842c9805e31092f44dedb218120fb187e Sign.typ_equiv; diff -r f753592842c9 -r a21431e996bf src/HOL/Tools/specification_package.ML --- a/src/HOL/Tools/specification_package.ML Thu Apr 13 11:22:44 2006 +0200 +++ b/src/HOL/Tools/specification_package.ML Thu Apr 13 12:00:50 2006 +0200 @@ -123,8 +123,6 @@ | myfoldr f (x::xs) = f (x,myfoldr f xs) | myfoldr f [] = error "SpecificationPackage.process_spec internal error" - fun typ_equiv t u = Sign.typ_instance thy (t,u) andalso Sign.typ_instance thy (u,t); - val rew_imps = alt_props |> map (ObjectLogic.atomize_cterm o Thm.read_cterm thy o rpair Term.propT o snd) val props' = rew_imps |> @@ -160,7 +158,7 @@ val (cname,ctyp) = dest_Const c' in case List.filter (fn t => let val (name,typ) = dest_Const t - in name = cname andalso typ_equiv typ ctyp + in name = cname andalso Sign.typ_equiv thy (typ, ctyp) end) thawed_prop_consts of [] => error ("Specification: No suitable instances of constant \"" ^ (Sign.string_of_term thy c) ^ "\" found") | [cf] => unvarify cf vmap