# HG changeset patch # User berghofe # Date 1114102638 -7200 # Node ID 5de27a5fc5edbeffec24af3e91cd183f1998eb7a # Parent acfdd493f5c4c69ce1b4346fa11d34168e2ec4fa Adapted to new interface of instantiation and unification / matching functions. diff -r acfdd493f5c4 -r 5de27a5fc5ed src/HOL/Import/proof_kernel.ML --- a/src/HOL/Import/proof_kernel.ML Thu Apr 21 18:56:03 2005 +0200 +++ b/src/HOL/Import/proof_kernel.ML Thu Apr 21 18:57:18 2005 +0200 @@ -1362,10 +1362,10 @@ val tys_before = add_term_tfrees (prop_of th,[]) val th1 = varifyT th val tys_after = add_term_tvars (prop_of th1,[]) - val tyinst = map (fn (bef,(i,_)) => + val tyinst = map (fn (bef, iS) => (case try (Lib.assoc (TFree bef)) lambda of - SOME ty => (i,ctyp_of sg ty) - | NONE => (i,ctyp_of sg (TFree bef)) + SOME ty => (ctyp_of sg (TVar iS), ctyp_of sg ty) + | NONE => (ctyp_of sg (TVar iS), ctyp_of sg (TFree bef)) )) (zip tys_before tys_after) val res = Drule.instantiate (tyinst,[]) th1 diff -r acfdd493f5c4 -r 5de27a5fc5ed src/HOL/Import/shuffler.ML --- a/src/HOL/Import/shuffler.ML Thu Apr 21 18:56:03 2005 +0200 +++ b/src/HOL/Import/shuffler.ML Thu Apr 21 18:57:18 2005 +0200 @@ -268,12 +268,14 @@ | inst_tfrees sg ((name,U)::rest) thm = let val cU = ctyp_of sg U - val tfree_names = add_term_tfree_names (prop_of thm,[]) - val (thm',rens) = varifyT' (tfree_names \ name) thm + val tfrees = add_term_tfrees (prop_of thm,[]) + val (thm',rens) = varifyT' + (gen_rem (op = o apfst fst) (tfrees, name)) thm val mid = case rens of [] => thm' - | [(_,idx)] => instantiate ([(idx,cU)],[]) thm' + | [((_, S), idx)] => instantiate + ([(ctyp_of sg (TVar (idx, S)), cU)], []) thm' | _ => error "Shuffler.inst_tfrees internal error" in inst_tfrees sg rest mid diff -r acfdd493f5c4 -r 5de27a5fc5ed src/HOL/Tools/ATP/recon_translate_proof.ML --- a/src/HOL/Tools/ATP/recon_translate_proof.ML Thu Apr 21 18:56:03 2005 +0200 +++ b/src/HOL/Tools/ATP/recon_translate_proof.ML Thu Apr 21 18:57:18 2005 +0200 @@ -122,7 +122,7 @@ (*******************************************) fun mksubstlist [] sublist = sublist - |mksubstlist ((a,b)::rest) sublist = let val vartype = type_of b + |mksubstlist ((a, (_, b)) :: rest) sublist = let val vartype = type_of b val avar = Var(a,vartype) val newlist = ((avar,b)::sublist) in mksubstlist rest newlist diff -r acfdd493f5c4 -r 5de27a5fc5ed src/HOL/Tools/inductive_package.ML --- a/src/HOL/Tools/inductive_package.ML Thu Apr 21 18:56:03 2005 +0200 +++ b/src/HOL/Tools/inductive_package.ML Thu Apr 21 18:57:18 2005 +0200 @@ -193,10 +193,8 @@ (env, (replicate (length consts) cT) ~~ consts) end; val (env, _) = Library.foldl unify ((Vartab.empty, i'), rec_consts); - fun typ_subst_TVars_2 env T = let val T' = typ_subst_TVars_Vartab env T - in if T = T' then T else typ_subst_TVars_2 env T' end; val subst = fst o Type.freeze_thaw o - (map_term_types (typ_subst_TVars_2 env)) + (map_term_types (Envir.norm_type env)) in (map subst cs', map subst intr_ts') end) handle Type.TUNIFY => diff -r acfdd493f5c4 -r 5de27a5fc5ed src/HOL/Tools/reconstruction.ML --- a/src/HOL/Tools/reconstruction.ML Thu Apr 21 18:56:03 2005 +0200 +++ b/src/HOL/Tools/reconstruction.ML Thu Apr 21 18:57:18 2005 +0200 @@ -16,7 +16,7 @@ (**************************************************************) fun mksubstlist [] sublist = sublist - | mksubstlist ((a,b)::rest) sublist = + | mksubstlist ((a, (_, b)) :: rest) sublist = let val vartype = type_of b val avar = Var(a,vartype) val newlist = ((avar,b)::sublist) diff -r acfdd493f5c4 -r 5de27a5fc5ed src/HOL/Tools/refute.ML --- a/src/HOL/Tools/refute.ML Thu Apr 21 18:56:03 2005 +0200 +++ b/src/HOL/Tools/refute.ML Thu Apr 21 18:57:18 2005 +0200 @@ -448,8 +448,8 @@ in map_term_types (map_type_tvar - (fn (v,_) => - case Vartab.lookup (typeSubs, v) of + (fn v => + case Type.lookup (typeSubs, v) of NONE => (* schematic type variable not instantiated *) raise REFUTE ("collect_axioms", "term " ^ Sign.string_of_term (sign_of thy) t ^ " still has a polymorphic type (after instantiating type of " ^ quote s ^ ")") @@ -459,11 +459,11 @@ end (* applies a type substitution 'typeSubs' for all type variables in a *) (* term 't' *) - (* Term.typ Term.Vartab.table -> Term.term -> Term.term *) + (* (Term.sort * Term.typ) Term.Vartab.table -> Term.term -> Term.term *) fun monomorphic_term typeSubs t = map_term_types (map_type_tvar - (fn (v, _) => - case Vartab.lookup (typeSubs, v) of + (fn v => + case Type.lookup (typeSubs, v) of NONE => (* schematic type variable not instantiated *) raise ERROR @@ -483,11 +483,11 @@ (* (string * Term.term) list *) val monomorphic_class_axioms = map (fn (axname, ax) => let - val (idx, _) = (case term_tvars ax of + val (idx, S) = (case term_tvars ax of [is] => is | _ => raise REFUTE ("collect_axioms", "class axiom " ^ axname ^ " (" ^ Sign.string_of_term (sign_of thy) ax ^ ") does not contain exactly one type variable")) in - (axname, monomorphic_term (Vartab.make [(idx, T)]) ax) + (axname, monomorphic_term (Vartab.make [(idx, (S, T))]) ax) end) class_axioms (* Term.term list * (string * Term.term) list -> Term.term list *) fun collect_axiom (axs, (axname, ax)) = diff -r acfdd493f5c4 -r 5de27a5fc5ed src/HOL/Tools/specification_package.ML --- a/src/HOL/Tools/specification_package.ML Thu Apr 21 18:56:03 2005 +0200 +++ b/src/HOL/Tools/specification_package.ML Thu Apr 21 18:57:18 2005 +0200 @@ -110,7 +110,7 @@ fun unthaw (f as (a,S)) = (case assoc (fmap',a) of NONE => TVar f - | SOME b => TFree (b,S)) + | SOME (b, _) => TFree (b,S)) in map_term_types (map_type_tvar unthaw) t end diff -r acfdd493f5c4 -r 5de27a5fc5ed src/HOLCF/adm.ML --- a/src/HOLCF/adm.ML Thu Apr 21 18:56:03 2005 +0200 +++ b/src/HOLCF/adm.ML Thu Apr 21 18:57:18 2005 +0200 @@ -125,10 +125,11 @@ 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' = Vartab.dest (Type.typ_match tsig (tye, (PT, #T (rep_cterm Pt)))); - val ctye = map (fn (x, y) => (x, ctyp_of sign y)) tye'; - val tv = cterm_of sign (Var (("t", j), typ_subst_TVars tye' tT)); - val Pv = cterm_of sign (Var (("P", j), typ_subst_TVars tye' PT)); + val tye' = Type.typ_match tsig (tye, (PT, #T (rep_cterm Pt))); + 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)); + val Pv = cterm_of sign (Var (("P", j), Envir.typ_subst_TVars tye' PT)); val rule' = instantiate (ctye, [(tv, tt), (Pv, Pt)]) rule in rule' end; diff -r acfdd493f5c4 -r 5de27a5fc5ed src/Provers/induct_method.ML --- a/src/Provers/induct_method.ML Thu Apr 21 18:56:03 2005 +0200 +++ b/src/Provers/induct_method.ML Thu Apr 21 18:57:18 2005 +0200 @@ -191,12 +191,13 @@ (* divinate rule instantiation (cannot handle pending goal parameters) *) -fun dest_env sign (env as Envir.Envir {asol, iTs, ...}) = +fun dest_env sign (env as Envir.Envir {iTs, ...}) = let - val pairs = Vartab.dest asol; - val ts = map (Thm.cterm_of sign o Envir.norm_term env o #2) pairs; + val pairs = Envir.alist_of env; + val ts = map (Thm.cterm_of sign o Envir.norm_term env o #2 o #2) pairs; val xs = map2 (Thm.cterm_of sign o Var) (map #1 pairs, map (#T o Thm.rep_cterm) ts); - in (map (apsnd (Thm.ctyp_of sign)) (Vartab.dest iTs), xs ~~ ts) end; + val cert = Thm.ctyp_of sign; + in (map (fn (ixn, (S, T)) => (cert (TVar (ixn, S)), cert T)) (Vartab.dest iTs), xs ~~ ts) end; fun divinate_inst rule i st = let