src/HOL/Tools/specification_package.ML
changeset 14769 b698d0b243dc
parent 14620 1be590fd2422
child 15531 08c8dad8e399
--- 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"]