# 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