--- 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