--- 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"]
--- 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)));