# HG changeset patch # User wenzelm # Date 1122556791 -7200 # Node ID 4d7f19d340e827e4cdf8ee4b0f8335174860e46a # Parent 9ef19e3c7fdd155ca274c28a25809476d0733712 Sign.typ_match; diff -r 9ef19e3c7fdd -r 4d7f19d340e8 TFL/casesplit.ML --- 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); diff -r 9ef19e3c7fdd -r 4d7f19d340e8 TFL/thry.ML --- 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; diff -r 9ef19e3c7fdd -r 4d7f19d340e8 src/HOL/Tools/refute.ML --- 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 diff -r 9ef19e3c7fdd -r 4d7f19d340e8 src/HOLCF/adm_tac.ML --- 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)); diff -r 9ef19e3c7fdd -r 4d7f19d340e8 src/Provers/splitter.ML --- 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