Adapted to new interface of instantiation and unification / matching functions.
--- 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
--- 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
--- 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
--- 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 =>
--- 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)
--- 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)) =
--- 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
--- 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;
--- 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