# HG changeset patch
# User wenzelm
# Date 1085166945 -7200
# Node ID b698d0b243dc86d71eb3bd95c595087b750a2215
# Parent  68496ae6640509d4e8f7315140f9e35ff18a5860
Sign.typ_instance;

diff -r 68496ae66405 -r b698d0b243dc src/HOL/Tools/specification_package.ML
--- a/src/HOL/Tools/specification_package.ML	Fri May 21 21:15:22 2004 +0200
+++ b/src/HOL/Tools/specification_package.ML	Fri May 21 21:15:45 2004 +0200
@@ -128,13 +128,7 @@
 	  | myfoldr f [] = error "SpecificationPackage.process_spec internal error"
 
 	val sg = sign_of thy
-	fun typ_equiv t u =
-	    let
-		val tsig = Sign.tsig_of sg
-	    in
-		Type.typ_instance(tsig,t,u) andalso
-		Type.typ_instance(tsig,u,t)
-	    end
+	fun typ_equiv t u = Sign.typ_instance sg (t,u) andalso Sign.typ_instance sg (u,t);
 
 	val cprops = map (Thm.read_cterm sg o rpair Term.propT o snd) alt_props
 	val ss = empty_ss setmksimps single addsimps [thm "HOL.atomize_imp",thm "HOL.atomize_all"]
diff -r 68496ae66405 -r b698d0b243dc src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Fri May 21 21:15:22 2004 +0200
+++ b/src/Pure/codegen.ML	Fri May 21 21:15:45 2004 +0200
@@ -236,7 +236,7 @@
                 None => T
               | Some ty =>
                   let val U = prep_type sg ty
-                  in if Type.typ_instance (Sign.tsig_of sg, U, T) then U
+                  in if Sign.typ_instance sg (U, T) then U
                     else error ("Illegal type constraint for constant " ^ cname)
                   end)
          in (case assoc (consts, (cname, T')) of
@@ -314,7 +314,7 @@
 (**** retrieve definition of constant ****)
 
 fun is_instance thy T1 T2 =
-  Type.typ_instance (Sign.tsig_of (sign_of thy), T1, Type.varifyT T2);
+  Sign.typ_instance (sign_of thy) (T1, Type.varifyT T2);
 
 fun get_assoc_code thy s T = apsome snd (find_first (fn ((s', T'), _) =>
   s = s' andalso is_instance thy T T') (#consts (CodegenData.get thy)));