--- a/TFL/casesplit.ML Thu Jul 28 15:19:49 2005 +0200
+++ b/TFL/casesplit.ML Thu Jul 28 15:19:51 2005 +0200
@@ -156,13 +156,12 @@
val casethm_vars = rev (Term.term_vars (Thm.concl_of case_thm));
- val tsig = Sign.tsig_of sgn;
val casethm_tvars = Term.term_tvars (Thm.concl_of case_thm);
val (Pv, Dv, type_insts) =
case (Thm.concl_of case_thm) of
(_ $ ((Pv as Var(P,Pty)) $ (Dv as Var(D, Dty)))) =>
(Pv, Dv,
- Type.typ_match tsig (Vartab.empty, (Dty, ty)))
+ Sign.typ_match sgn (Dty, ty) Vartab.empty)
| _ => raise ERROR_MESSAGE ("not a valid case thm");
val type_cinsts = map (fn (ixn, (S, T)) => (ctypify (TVar (ixn, S)), ctypify T))
(Vartab.dest type_insts);
--- a/TFL/thry.ML Thu Jul 28 15:19:49 2005 +0200
+++ b/TFL/thry.ML Thu Jul 28 15:19:51 2005 +0200
@@ -40,8 +40,8 @@
in (map tmbind (Vartab.dest tm_theta), map tybind (Vartab.dest ty_theta))
end;
-fun match_type thry pat ob = map tybind (Vartab.dest
- (Type.typ_match (Sign.tsig_of (Theory.sign_of thry)) (Vartab.empty, (pat, ob))));
+fun match_type thry pat ob =
+ map tybind (Vartab.dest (Sign.typ_match thry (pat, ob) Vartab.empty));
end;
--- a/src/HOL/Tools/refute.ML Thu Jul 28 15:19:49 2005 +0200
+++ b/src/HOL/Tools/refute.ML Thu Jul 28 15:19:51 2005 +0200
@@ -434,7 +434,7 @@
let
fun find_typeSubs (Const (s', T')) =
(if s=s' then
- SOME (Type.typ_match (Sign.tsig_of (sign_of thy)) (Vartab.empty, (T', T))) handle Type.TYPE_MATCH => NONE
+ SOME (Sign.typ_match thy (T', T) Vartab.empty) handle Type.TYPE_MATCH => NONE
else
NONE)
| find_typeSubs (Free _) = NONE
@@ -543,7 +543,7 @@
SOME T' =>
let
val T'' = (domain_type o domain_type) T'
- val typeSubs = Type.typ_match (Sign.tsig_of (sign_of thy)) (Vartab.empty, (T'', T))
+ val typeSubs = Sign.typ_match thy (T'', T) Vartab.empty
in
SOME (axname, monomorphic_term typeSubs ax)
end
@@ -642,7 +642,7 @@
in
if s=s' then
let
- val typeSubs = Type.typ_match (Sign.tsig_of (sign_of thy)) (Vartab.empty, (T', T))
+ val typeSubs = Sign.typ_match thy (T', T) Vartab.empty
in
SOME (axname, monomorphic_term typeSubs ax)
end
@@ -668,7 +668,7 @@
Library.exists (fn c =>
(case c of
Const (cname, ctype) =>
- cname = s andalso Type.typ_instance (Sign.tsig_of (sign_of thy)) (T, ctype)
+ cname = s andalso Sign.typ_instance thy (T, ctype)
| _ =>
raise REFUTE ("collect_axioms", "IDT constructor is not a constant")))
constrs
@@ -1738,7 +1738,7 @@
())
(* split the constructors into those occuring before/after 'Const (s, T)' *)
val (constrs1, constrs2) = take_prefix (fn (cname, ctypes) =>
- not (cname = s andalso Type.typ_instance (Sign.tsig_of (sign_of thy)) (T,
+ not (cname = s andalso Sign.typ_instance thy (T,
map (typ_of_dtyp descr typ_assoc) ctypes ---> Type (s', Ts')))) constrs
in
case constrs2 of
--- a/src/HOLCF/adm_tac.ML Thu Jul 28 15:19:49 2005 +0200
+++ b/src/HOLCF/adm_tac.ML Thu Jul 28 15:19:51 2005 +0200
@@ -112,7 +112,6 @@
fun inst_adm_subst_thm state i params s T subt t paths =
let val {sign, maxidx, ...} = rep_thm state;
val j = maxidx+1;
- val tsig = Sign.tsig_of sign;
val parTs = map snd (rev params);
val rule = lift_rule (state, i) adm_subst;
val types = valOf o (fst (types_sorts rule));
@@ -123,8 +122,8 @@
val tt = cterm_of sign (mk_abs (params @ [(s, T)]) subt);
val Pt = cterm_of sign (mk_abs (params @ [(s, fastype_of1 (T::parTs, subt))])
(make_term t [] paths 0));
- val tye = Type.typ_match tsig (Vartab.empty, (tT, #T (rep_cterm tt)));
- val tye' = Type.typ_match tsig (tye, (PT, #T (rep_cterm Pt)));
+ val tye = Sign.typ_match sign (tT, #T (rep_cterm tt)) Vartab.empty;
+ val tye' = Sign.typ_match sign (PT, #T (rep_cterm Pt)) tye;
val ctye = map (fn (ixn, (S, T)) =>
(ctyp_of sign (TVar (ixn, S)), ctyp_of sign T)) (Vartab.dest tye');
val tv = cterm_of sign (Var (("t", j), Envir.typ_subst_TVars tye' tT));
--- a/src/Provers/splitter.ML Thu Jul 28 15:19:49 2005 +0200
+++ b/src/Provers/splitter.ML Thu Jul 28 15:19:51 2005 +0200
@@ -202,19 +202,19 @@
local
exception MATCH
in
-fun typ_match tsig args = (Type.typ_match tsig args)
+fun typ_match sg (tyenv, TU) = (Sign.typ_match sg TU tyenv)
handle Type.TYPE_MATCH => raise MATCH;
-fun fomatch tsig args =
+fun fomatch sg args =
let
fun mtch tyinsts = fn
- (Ts,Var(_,T), t) => typ_match tsig (tyinsts, (T, fastype_of1(Ts,t)))
+ (Ts,Var(_,T), t) => typ_match sg (tyinsts, (T, fastype_of1(Ts,t)))
| (_,Free (a,T), Free (b,U)) =>
- if a=b then typ_match tsig (tyinsts,(T,U)) else raise MATCH
+ if a=b then typ_match sg (tyinsts,(T,U)) else raise MATCH
| (_,Const (a,T), Const (b,U)) =>
- if a=b then typ_match tsig (tyinsts,(T,U)) else raise MATCH
+ if a=b then typ_match sg (tyinsts,(T,U)) else raise MATCH
| (_,Bound i, Bound j) => if i=j then tyinsts else raise MATCH
| (Ts,Abs(_,T,t), Abs(_,U,u)) =>
- mtch (typ_match tsig (tyinsts,(T,U))) (U::Ts,t,u)
+ mtch (typ_match sg (tyinsts,(T,U))) (U::Ts,t,u)
| (Ts, f$t, g$u) => mtch (mtch tyinsts (Ts,f,g)) (Ts, t, u)
| _ => raise MATCH
in (mtch Vartab.empty args; true) handle MATCH => false end;
@@ -236,7 +236,7 @@
| find ((gcT, pat, thm, T, n)::tups) =
let val t2 = list_comb (h, Library.take (n, ts))
in if Sign.typ_instance sg (cT, gcT)
- andalso fomatch (Sign.tsig_of sg) (Ts,pat,t2)
+ andalso fomatch sg (Ts,pat,t2)
then mk_split_pack(thm,T,T',n,ts,apsns,pos,type_of1(Ts,t2),t2)
else find tups
end