tuned/modernized Envir operations;
authorwenzelm
Fri Jul 17 21:33:00 2009 +0200 (2009-07-17)
changeset 32032a6a6e8031c14
parent 32031 e2e6b0691264
child 32033 f92df23c3305
tuned/modernized Envir operations;
src/HOL/Library/reflection.ML
src/HOL/Tools/meson.ML
src/Pure/Isar/proof_context.ML
src/Pure/Proof/extraction.ML
src/Pure/Proof/reconstruct.ML
src/Pure/pattern.ML
src/Pure/proofterm.ML
src/Pure/thm.ML
src/Pure/unify.ML
src/Tools/eqsubst.ML
src/Tools/induct.ML
     1.1 --- a/src/HOL/Library/reflection.ML	Fri Jul 17 21:33:00 2009 +0200
     1.2 +++ b/src/HOL/Library/reflection.ML	Fri Jul 17 21:33:00 2009 +0200
     1.3 @@ -153,8 +153,8 @@
     1.4              val certy = ctyp_of thy
     1.5              val (tyenv, tmenv) =
     1.6                Pattern.match thy
     1.7 -              ((fst o HOLogic.dest_eq o HOLogic.dest_Trueprop) (concl_of cong), t)
     1.8 -              (Envir.type_env (Envir.empty 0), Vartab.empty)
     1.9 +                ((fst o HOLogic.dest_eq o HOLogic.dest_Trueprop) (concl_of cong), t)
    1.10 +                (Vartab.empty, Vartab.empty)
    1.11              val (fnvs,invs) = List.partition (fn ((vn,_),_) => vn mem vns) (Vartab.dest tmenv)
    1.12              val (fts,its) =
    1.13  	      (map (snd o snd) fnvs,
    1.14 @@ -204,9 +204,7 @@
    1.15              val xns_map = (fst (split_list nths)) ~~ xns
    1.16              val subst = map (fn (nt, xn) => (nt, Var ((xn,0), fastype_of nt))) xns_map
    1.17              val rhs_P = subst_free subst rhs
    1.18 -            val (tyenv, tmenv) = Pattern.match
    1.19 -                              thy (rhs_P, t)
    1.20 -                              (Envir.type_env (Envir.empty 0), Vartab.empty)
    1.21 +            val (tyenv, tmenv) = Pattern.match thy (rhs_P, t) (Vartab.empty, Vartab.empty)
    1.22              val sbst = Envir.subst_vars (tyenv, tmenv)
    1.23              val sbsT = Envir.typ_subst_TVars tyenv
    1.24              val subst_ty = map (fn (n,(s,t)) => (certT (TVar (n, s)), certT t))
     2.1 --- a/src/HOL/Tools/meson.ML	Fri Jul 17 21:33:00 2009 +0200
     2.2 +++ b/src/HOL/Tools/meson.ML	Fri Jul 17 21:33:00 2009 +0200
     2.3 @@ -87,14 +87,12 @@
     2.4  fun typ_pair_of (ix, (sort,ty)) = (TVar (ix,sort), ty);
     2.5  fun term_pair_of (ix, (ty,t)) = (Var (ix,ty), t);
     2.6  
     2.7 -val Envir.Envir {asol = tenv0, iTs = tyenv0, ...} = Envir.empty 0
     2.8 -
     2.9  (*FIXME: currently does not "rename variables apart"*)
    2.10  fun first_order_resolve thA thB =
    2.11    let val thy = theory_of_thm thA
    2.12        val tmA = concl_of thA
    2.13        val Const("==>",_) $ tmB $ _ = prop_of thB
    2.14 -      val (tyenv,tenv) = Pattern.first_order_match thy (tmB,tmA) (tyenv0,tenv0)
    2.15 +      val (tyenv, tenv) = Pattern.first_order_match thy (tmB, tmA) (Vartab.empty, Vartab.empty)
    2.16        val ct_pairs = map (pairself (cterm_of thy) o term_pair_of) (Vartab.dest tenv)
    2.17    in  thA RS (cterm_instantiate ct_pairs thB)  end
    2.18    handle _ => raise THM ("first_order_resolve", 0, [thA,thB]);  (* FIXME avoid handle _ *)
    2.19 @@ -104,8 +102,8 @@
    2.20        [] => th
    2.21      | pairs =>
    2.22          let val thy = theory_of_thm th
    2.23 -            val (tyenv,tenv) =
    2.24 -                  List.foldl (uncurry (Pattern.first_order_match thy)) (tyenv0,tenv0) pairs
    2.25 +            val (tyenv, tenv) =
    2.26 +              fold (Pattern.first_order_match thy) pairs (Vartab.empty, Vartab.empty)
    2.27              val t_pairs = map term_pair_of (Vartab.dest tenv)
    2.28              val th' = Thm.instantiate ([], map (pairself (cterm_of thy)) t_pairs) th
    2.29          in  th'  end
     3.1 --- a/src/Pure/Isar/proof_context.ML	Fri Jul 17 21:33:00 2009 +0200
     3.2 +++ b/src/Pure/Isar/proof_context.ML	Fri Jul 17 21:33:00 2009 +0200
     3.3 @@ -779,7 +779,7 @@
     3.4  fun simult_matches ctxt (t, pats) =
     3.5    (case Seq.pull (Unify.matchers (theory_of ctxt) (map (rpair t) pats)) of
     3.6      NONE => error "Pattern match failed!"
     3.7 -  | SOME (env, _) => map (apsnd snd) (Envir.alist_of env));
     3.8 +  | SOME (env, _) => Vartab.fold (fn (v, (_, t)) => cons (v, t)) (Envir.term_env env) []);
     3.9  
    3.10  
    3.11  (* bind_terms *)
     4.1 --- a/src/Pure/Proof/extraction.ML	Fri Jul 17 21:33:00 2009 +0200
     4.2 +++ b/src/Pure/Proof/extraction.ML	Fri Jul 17 21:33:00 2009 +0200
     4.3 @@ -105,9 +105,8 @@
     4.4            val env as (Tenv, tenv) = Pattern.match thy (inc tm1, tm) (Vartab.empty, Vartab.empty);
     4.5            val prems' = map (pairself (Envir.subst_vars env o inc o ren)) prems;
     4.6            val env' = Envir.Envir
     4.7 -            {maxidx = Library.foldl Int.max
     4.8 -              (~1, map (Int.max o pairself maxidx_of_term) prems'),
     4.9 -             iTs = Tenv, asol = tenv};
    4.10 +            {maxidx = fold (fn (t, u) => Term.maxidx_term t #> Term.maxidx_term u) prems' ~1,
    4.11 +             tenv = tenv, tyenv = Tenv};
    4.12            val env'' = fold (Pattern.unify thy o pairself (lookup rew)) prems' env';
    4.13          in SOME (Envir.norm_term env'' (inc (ren tm2)))
    4.14          end handle Pattern.MATCH => NONE | Pattern.Unif => NONE)
     5.1 --- a/src/Pure/Proof/reconstruct.ML	Fri Jul 17 21:33:00 2009 +0200
     5.2 +++ b/src/Pure/Proof/reconstruct.ML	Fri Jul 17 21:33:00 2009 +0200
     5.3 @@ -35,12 +35,6 @@
     5.4  fun forall_intr_vfs_prf prop prf = fold_rev forall_intr_prf
     5.5    (vars_of prop @ frees_of prop) prf;
     5.6  
     5.7 -fun merge_envs (Envir.Envir {asol=asol1, iTs=iTs1, maxidx=maxidx1})
     5.8 -  (Envir.Envir {asol=asol2, iTs=iTs2, maxidx=maxidx2}) =
     5.9 -    Envir.Envir {asol=Vartab.merge (op =) (asol1, asol2),
    5.10 -                 iTs=Vartab.merge (op =) (iTs1, iTs2),
    5.11 -                 maxidx=Int.max (maxidx1, maxidx2)};
    5.12 -
    5.13  
    5.14  (**** generate constraints for proof term ****)
    5.15  
    5.16 @@ -48,31 +42,32 @@
    5.17    let val (env', v) = Envir.genvar "a" (env, rev Ts ---> T)
    5.18    in (env', list_comb (v, map Bound (length Ts - 1 downto 0))) end;
    5.19  
    5.20 -fun mk_tvar (Envir.Envir {iTs, asol, maxidx}, s) =
    5.21 -  (Envir.Envir {iTs = iTs, asol = asol, maxidx = maxidx+1},
    5.22 -   TVar (("'t", maxidx+1), s));
    5.23 +fun mk_tvar (Envir.Envir {maxidx, tenv, tyenv}, s) =
    5.24 +  (Envir.Envir {maxidx = maxidx + 1, tenv = tenv, tyenv = tyenv},
    5.25 +   TVar (("'t", maxidx + 1), s));
    5.26  
    5.27  val mk_abs = fold (fn T => fn u => Abs ("", T, u));
    5.28  
    5.29  fun unifyT thy env T U =
    5.30    let
    5.31 -    val Envir.Envir {asol, iTs, maxidx} = env;
    5.32 -    val (iTs', maxidx') = Sign.typ_unify thy (T, U) (iTs, maxidx)
    5.33 -  in Envir.Envir {asol=asol, iTs=iTs', maxidx=maxidx'} end
    5.34 -  handle Type.TUNIFY => error ("Non-unifiable types:\n" ^
    5.35 -    Syntax.string_of_typ_global thy T ^ "\n\n" ^ Syntax.string_of_typ_global thy U);
    5.36 +    val Envir.Envir {maxidx, tenv, tyenv} = env;
    5.37 +    val (tyenv', maxidx') = Sign.typ_unify thy (T, U) (tyenv, maxidx);
    5.38 +  in Envir.Envir {maxidx = maxidx', tenv = tenv, tyenv = tyenv'} end;
    5.39  
    5.40 -fun chaseT (env as Envir.Envir {iTs, ...}) (T as TVar ixnS) =
    5.41 -      (case Type.lookup iTs ixnS of NONE => T | SOME T' => chaseT env T')
    5.42 +fun chaseT env (T as TVar v) =
    5.43 +      (case Type.lookup (Envir.type_env env) v of
    5.44 +        NONE => T
    5.45 +      | SOME T' => chaseT env T')
    5.46    | chaseT _ T = T;
    5.47  
    5.48 -fun infer_type thy (env as Envir.Envir {maxidx, asol, iTs}) Ts vTs
    5.49 -      (t as Const (s, T)) = if T = dummyT then (case Sign.const_type thy s of
    5.50 +fun infer_type thy (env as Envir.Envir {maxidx, tenv, tyenv}) Ts vTs
    5.51 +      (t as Const (s, T)) = if T = dummyT then
    5.52 +        (case Sign.const_type thy s of
    5.53            NONE => error ("reconstruct_proof: No such constant: " ^ quote s)
    5.54          | SOME T =>
    5.55              let val T' = Type.strip_sorts (Logic.incr_tvar (maxidx + 1) T)
    5.56              in (Const (s, T'), T', vTs,
    5.57 -              Envir.Envir {maxidx = maxidx + 1, asol = asol, iTs = iTs})
    5.58 +              Envir.Envir {maxidx = maxidx + 1, tenv = tenv, tyenv = tyenv})
    5.59              end)
    5.60        else (t, T, vTs, env)
    5.61    | infer_type thy env Ts vTs (t as Free (s, T)) =
    5.62 @@ -236,21 +231,23 @@
    5.63  
    5.64  fun upd_constrs env cs =
    5.65    let
    5.66 -    val Envir.Envir {asol, iTs, ...} = env;
    5.67 +    val tenv = Envir.term_env env;
    5.68 +    val tyenv = Envir.type_env env;
    5.69      val dom = []
    5.70 -      |> Vartab.fold (cons o #1) asol
    5.71 -      |> Vartab.fold (cons o #1) iTs;
    5.72 +      |> Vartab.fold (cons o #1) tenv
    5.73 +      |> Vartab.fold (cons o #1) tyenv;
    5.74      val vran = []
    5.75 -      |> Vartab.fold (Term.add_var_names o #2 o #2) asol
    5.76 -      |> Vartab.fold (Term.add_tvar_namesT o #2 o #2) iTs;
    5.77 +      |> Vartab.fold (Term.add_var_names o #2 o #2) tenv
    5.78 +      |> Vartab.fold (Term.add_tvar_namesT o #2 o #2) tyenv;
    5.79      fun check_cs [] = []
    5.80 -      | check_cs ((u, p, vs)::ps) =
    5.81 -          let val vs' = subtract (op =) dom vs;
    5.82 -          in if vs = vs' then (u, p, vs)::check_cs ps
    5.83 -             else (true, p, fold (insert (op =)) vs' vran)::check_cs ps
    5.84 -          end
    5.85 +      | check_cs ((u, p, vs) :: ps) =
    5.86 +          let val vs' = subtract (op =) dom vs in
    5.87 +            if vs = vs' then (u, p, vs) :: check_cs ps
    5.88 +            else (true, p, fold (insert op =) vs' vran) :: check_cs ps
    5.89 +          end;
    5.90    in check_cs cs end;
    5.91  
    5.92 +
    5.93  (**** solution of constraints ****)
    5.94  
    5.95  fun solve _ [] bigenv = bigenv
    5.96 @@ -280,7 +277,7 @@
    5.97          val Envir.Envir {maxidx, ...} = bigenv;
    5.98          val (env, cs') = search (Envir.empty maxidx) cs;
    5.99        in
   5.100 -        solve thy (upd_constrs env cs') (merge_envs bigenv env)
   5.101 +        solve thy (upd_constrs env cs') (Envir.merge (bigenv, env))
   5.102        end;
   5.103  
   5.104  
     6.1 --- a/src/Pure/pattern.ML	Fri Jul 17 21:33:00 2009 +0200
     6.2 +++ b/src/Pure/pattern.ML	Fri Jul 17 21:33:00 2009 +0200
     6.3 @@ -141,8 +141,10 @@
     6.4    | split_type (Type ("fun",[T1,T2]),n,Ts) = split_type (T2,n-1,T1::Ts)
     6.5    | split_type _                           = error("split_type");
     6.6  
     6.7 -fun type_of_G (env as Envir.Envir {iTs, ...}) (T,n,is) =
     6.8 -  let val (Ts, U) = split_type (Envir.norm_type iTs T, n, [])
     6.9 +fun type_of_G env (T, n, is) =
    6.10 +  let
    6.11 +    val tyenv = Envir.type_env env;
    6.12 +    val (Ts, U) = split_type (Envir.norm_type tyenv T, n, []);
    6.13    in map (nth Ts) is ---> U end;
    6.14  
    6.15  fun mkhnf (binders,is,G,js) = mkabs (binders, is, app(G,js));
    6.16 @@ -225,11 +227,12 @@
    6.17                   end;
    6.18    in if TermOrd.indexname_ord (G,F) = LESS then ff(F,Fty,is,G,Gty,js) else ff(G,Gty,js,F,Fty,is) end
    6.19  
    6.20 -fun unify_types thy (T,U) (env as Envir.Envir{asol,iTs,maxidx}) =
    6.21 -  if T=U then env
    6.22 -  else let val (iTs',maxidx') = Sign.typ_unify thy (U, T) (iTs, maxidx)
    6.23 -       in Envir.Envir{asol=asol,maxidx=maxidx',iTs=iTs'} end
    6.24 -       handle Type.TUNIFY => (typ_clash thy (iTs,T,U); raise Unif);
    6.25 +fun unify_types thy (T, U) (env as Envir.Envir {maxidx, tenv, tyenv}) =
    6.26 +  if T = U then env
    6.27 +  else
    6.28 +    let val (tyenv', maxidx') = Sign.typ_unify thy (U, T) (tyenv, maxidx)
    6.29 +    in Envir.Envir {maxidx = maxidx', tenv = tenv, tyenv = tyenv'} end
    6.30 +    handle Type.TUNIFY => (typ_clash thy (tyenv, T, U); raise Unif);
    6.31  
    6.32  fun unif thy binders (s,t) env = case (Envir.head_norm env s, Envir.head_norm env t) of
    6.33        (Abs(ns,Ts,ts),Abs(nt,Tt,tt)) =>
     7.1 --- a/src/Pure/proofterm.ML	Fri Jul 17 21:33:00 2009 +0200
     7.2 +++ b/src/Pure/proofterm.ML	Fri Jul 17 21:33:00 2009 +0200
     7.3 @@ -489,9 +489,8 @@
     7.4    | remove_types (Const (s, _)) = Const (s, dummyT)
     7.5    | remove_types t = t;
     7.6  
     7.7 -fun remove_types_env (Envir.Envir {iTs, asol, maxidx}) =
     7.8 -  Envir.Envir {iTs = iTs, asol = Vartab.map (apsnd remove_types) asol,
     7.9 -    maxidx = maxidx};
    7.10 +fun remove_types_env (Envir.Envir {maxidx, tenv, tyenv}) =
    7.11 +  Envir.Envir {maxidx = maxidx, tenv = Vartab.map (apsnd remove_types) tenv, tyenv = tyenv};
    7.12  
    7.13  fun norm_proof' env prf = norm_proof (remove_types_env env) prf;
    7.14  
     8.1 --- a/src/Pure/thm.ML	Fri Jul 17 21:33:00 2009 +0200
     8.2 +++ b/src/Pure/thm.ML	Fri Jul 17 21:33:00 2009 +0200
     8.3 @@ -1247,12 +1247,12 @@
     8.4      val Thm (der, {thy_ref, maxidx, shyps, hyps, prop, ...}) = state;
     8.5      val thy = Theory.deref thy_ref;
     8.6      val (tpairs, Bs, Bi, C) = dest_state (state, i);
     8.7 -    fun newth n (env as Envir.Envir {maxidx, ...}, tpairs) =
     8.8 +    fun newth n (env, tpairs) =
     8.9        Thm (deriv_rule1
    8.10            ((if Envir.is_empty env then I else (Pt.norm_proof' env)) o
    8.11              Pt.assumption_proof Bs Bi n) der,
    8.12         {tags = [],
    8.13 -        maxidx = maxidx,
    8.14 +        maxidx = Envir.maxidx_of env,
    8.15          shyps = Envir.insert_sorts env shyps,
    8.16          hyps = hyps,
    8.17          tpairs =
    8.18 @@ -1465,15 +1465,15 @@
    8.19  
    8.20  (*Faster normalization: skip assumptions that were lifted over*)
    8.21  fun norm_term_skip env 0 t = Envir.norm_term env t
    8.22 -  | norm_term_skip env n (Const("all",_)$Abs(a,T,t)) =
    8.23 -        let val Envir.Envir{iTs, ...} = env
    8.24 -            val T' = Envir.typ_subst_TVars iTs T
    8.25 -            (*Must instantiate types of parameters because they are flattened;
    8.26 -              this could be a NEW parameter*)
    8.27 -        in Term.all T' $ Abs(a, T', norm_term_skip env n t)  end
    8.28 -  | norm_term_skip env n (Const("==>", _) $ A $ B) =
    8.29 -        Logic.mk_implies (A, norm_term_skip env (n-1) B)
    8.30 -  | norm_term_skip env n t = error"norm_term_skip: too few assumptions??";
    8.31 +  | norm_term_skip env n (Const ("all", _) $ Abs (a, T, t)) =
    8.32 +      let
    8.33 +        val T' = Envir.typ_subst_TVars (Envir.type_env env) T
    8.34 +        (*Must instantiate types of parameters because they are flattened;
    8.35 +          this could be a NEW parameter*)
    8.36 +      in Term.all T' $ Abs (a, T', norm_term_skip env n t) end
    8.37 +  | norm_term_skip env n (Const ("==>", _) $ A $ B) =
    8.38 +      Logic.mk_implies (A, norm_term_skip env (n - 1) B)
    8.39 +  | norm_term_skip env n t = error "norm_term_skip: too few assumptions??";
    8.40  
    8.41  
    8.42  (*Composition of object rule r=(A1...Am/B) with proof state s=(B1...Bn/C)
    8.43 @@ -1495,7 +1495,7 @@
    8.44       and nlift = Logic.count_prems (strip_all_body Bi) + (if eres_flg then ~1 else 0)
    8.45       val thy = Theory.deref (merge_thys2 state orule);
    8.46       (** Add new theorem with prop = '[| Bs; As |] ==> C' to thq **)
    8.47 -     fun addth A (As, oldAs, rder', n) ((env as Envir.Envir {maxidx, ...}, tpairs), thq) =
    8.48 +     fun addth A (As, oldAs, rder', n) ((env, tpairs), thq) =
    8.49         let val normt = Envir.norm_term env;
    8.50             (*perform minimal copying here by examining env*)
    8.51             val (ntpairs, normp) =
    8.52 @@ -1520,7 +1520,7 @@
    8.53                         curry op oo (Pt.norm_proof' env))
    8.54                      (Pt.bicompose_proof flatten Bs oldAs As A n (nlift+1))) rder' sder,
    8.55                  {tags = [],
    8.56 -                 maxidx = maxidx,
    8.57 +                 maxidx = Envir.maxidx_of env,
    8.58                   shyps = Envir.insert_sorts env (Sorts.union rshyps sshyps),
    8.59                   hyps = union_hyps rhyps shyps,
    8.60                   tpairs = ntpairs,
     9.1 --- a/src/Pure/unify.ML	Fri Jul 17 21:33:00 2009 +0200
     9.2 +++ b/src/Pure/unify.ML	Fri Jul 17 21:33:00 2009 +0200
     9.3 @@ -52,36 +52,48 @@
     9.4  
     9.5  type dpair = binderlist * term * term;
     9.6  
     9.7 -fun body_type(Envir.Envir{iTs,...}) =
     9.8 -let fun bT(Type("fun",[_,T])) = bT T
     9.9 -      | bT(T as TVar ixnS) = (case Type.lookup iTs ixnS of
    9.10 -    NONE => T | SOME(T') => bT T')
    9.11 -      | bT T = T
    9.12 -in bT end;
    9.13 +fun body_type env =
    9.14 +  let
    9.15 +    val tyenv = Envir.type_env env;
    9.16 +    fun bT (Type ("fun", [_, T])) = bT T
    9.17 +      | bT (T as TVar v) =
    9.18 +          (case Type.lookup tyenv v of
    9.19 +            NONE => T
    9.20 +          | SOME T' => bT T')
    9.21 +      | bT T = T;
    9.22 +  in bT end;
    9.23  
    9.24 -fun binder_types(Envir.Envir{iTs,...}) =
    9.25 -let fun bTs(Type("fun",[T,U])) = T :: bTs U
    9.26 -      | bTs(T as TVar ixnS) = (case Type.lookup iTs ixnS of
    9.27 -    NONE => [] | SOME(T') => bTs T')
    9.28 -      | bTs _ = []
    9.29 -in bTs end;
    9.30 +fun binder_types env =
    9.31 +  let
    9.32 +    val tyenv = Envir.type_env env;
    9.33 +    fun bTs (Type ("fun", [T, U])) = T :: bTs U
    9.34 +      | bTs (T as TVar v) =
    9.35 +          (case Type.lookup tyenv v of
    9.36 +            NONE => []
    9.37 +          | SOME T' => bTs T')
    9.38 +      | bTs _ = [];
    9.39 +  in bTs end;
    9.40  
    9.41  fun strip_type env T = (binder_types env T, body_type env T);
    9.42  
    9.43  fun fastype env (Ts, t) = Envir.fastype env (map snd Ts) t;
    9.44  
    9.45  
    9.46 -(*Eta normal form*)
    9.47 -fun eta_norm(env as Envir.Envir{iTs,...}) =
    9.48 -  let fun etif (Type("fun",[T,U]), t) =
    9.49 -      Abs("", T, etif(U, incr_boundvars 1 t $ Bound 0))
    9.50 -  | etif (TVar ixnS, t) =
    9.51 -      (case Type.lookup iTs ixnS of
    9.52 -      NONE => t | SOME(T) => etif(T,t))
    9.53 -  | etif (_,t) = t;
    9.54 -      fun eta_nm (rbinder, Abs(a,T,body)) =
    9.55 -      Abs(a, T, eta_nm ((a,T)::rbinder, body))
    9.56 -  | eta_nm (rbinder, t) = etif(fastype env (rbinder,t), t)
    9.57 +(* eta normal form *)
    9.58 +
    9.59 +fun eta_norm env =
    9.60 +  let
    9.61 +    val tyenv = Envir.type_env env;
    9.62 +    fun etif (Type ("fun", [T, U]), t) =
    9.63 +          Abs ("", T, etif (U, incr_boundvars 1 t $ Bound 0))
    9.64 +      | etif (TVar v, t) =
    9.65 +          (case Type.lookup tyenv v of
    9.66 +            NONE => t
    9.67 +          | SOME T => etif (T, t))
    9.68 +      | etif (_, t) = t;
    9.69 +    fun eta_nm (rbinder, Abs (a, T, body)) =
    9.70 +          Abs (a, T, eta_nm ((a, T) :: rbinder, body))
    9.71 +      | eta_nm (rbinder, t) = etif (fastype env (rbinder, t), t);
    9.72    in eta_nm end;
    9.73  
    9.74  
    9.75 @@ -186,11 +198,14 @@
    9.76  exception ASSIGN; (*Raised if not an assignment*)
    9.77  
    9.78  
    9.79 -fun unify_types thy (T,U, env as Envir.Envir{asol,iTs,maxidx}) =
    9.80 -  if T=U then env
    9.81 -  else let val (iTs',maxidx') = Sign.typ_unify thy (U, T) (iTs, maxidx)
    9.82 -       in Envir.Envir{asol=asol,maxidx=maxidx',iTs=iTs'} end
    9.83 -       handle Type.TUNIFY => raise CANTUNIFY;
    9.84 +fun unify_types thy (T, U, env) =
    9.85 +  if T = U then env
    9.86 +  else
    9.87 +    let
    9.88 +      val Envir.Envir {maxidx, tenv, tyenv} = env;
    9.89 +      val (tyenv', maxidx') = Sign.typ_unify thy (U, T) (tyenv, maxidx);
    9.90 +    in Envir.Envir {maxidx = maxidx', tenv = tenv, tyenv = tyenv'} end
    9.91 +    handle Type.TUNIFY => raise CANTUNIFY;
    9.92  
    9.93  fun test_unify_types thy (args as (T,U,_)) =
    9.94  let val str_of = Syntax.string_of_typ_global thy;
    9.95 @@ -636,9 +651,9 @@
    9.96  
    9.97  
    9.98  (*Pattern matching*)
    9.99 -fun first_order_matchers thy pairs (Envir.Envir {asol = tenv, iTs = tyenv, maxidx}) =
   9.100 +fun first_order_matchers thy pairs (Envir.Envir {maxidx, tenv, tyenv}) =
   9.101    let val (tyenv', tenv') = fold (Pattern.first_order_match thy) pairs (tyenv, tenv)
   9.102 -  in Seq.single (Envir.Envir {asol = tenv', iTs = tyenv', maxidx = maxidx}) end
   9.103 +  in Seq.single (Envir.Envir {maxidx = maxidx, tenv = tenv', tyenv = tyenv'}) end
   9.104    handle Pattern.MATCH => Seq.empty;
   9.105  
   9.106  (*General matching -- keeps variables disjoint*)
   9.107 @@ -661,10 +676,12 @@
   9.108            Term.map_aterms (fn t as Var ((x, i), T) =>
   9.109              if i > maxidx then Var ((x, i - offset), T) else t | t => t);
   9.110  
   9.111 -        fun norm_tvar (Envir.Envir {iTs = tyenv, ...}) ((x, i), S) =
   9.112 -          ((x, i - offset), (S, decr_indexesT (Envir.norm_type tyenv (TVar ((x, i), S)))));
   9.113 -        fun norm_var (env as Envir.Envir {iTs = tyenv, ...}) ((x, i), T) =
   9.114 +        fun norm_tvar env ((x, i), S) =
   9.115 +          ((x, i - offset),
   9.116 +            (S, decr_indexesT (Envir.norm_type (Envir.type_env env) (TVar ((x, i), S)))));
   9.117 +        fun norm_var env ((x, i), T) =
   9.118            let
   9.119 +            val tyenv = Envir.type_env env;
   9.120              val T' = Envir.norm_type tyenv T;
   9.121              val t' = Envir.norm_term env (Var ((x, i), T'));
   9.122            in ((x, i - offset), (decr_indexesT T', decr_indexes t')) end;
   9.123 @@ -672,8 +689,8 @@
   9.124          fun result env =
   9.125            if Envir.above env maxidx then   (* FIXME proper handling of generated vars!? *)
   9.126              SOME (Envir.Envir {maxidx = maxidx,
   9.127 -              iTs = Vartab.make (map (norm_tvar env) pat_tvars),
   9.128 -              asol = Vartab.make (map (norm_var env) pat_vars)})
   9.129 +              tyenv = Vartab.make (map (norm_tvar env) pat_tvars),
   9.130 +              tenv = Vartab.make (map (norm_var env) pat_vars)})
   9.131            else NONE;
   9.132  
   9.133          val empty = Envir.empty maxidx';
    10.1 --- a/src/Tools/eqsubst.ML	Fri Jul 17 21:33:00 2009 +0200
    10.2 +++ b/src/Tools/eqsubst.ML	Fri Jul 17 21:33:00 2009 +0200
    10.3 @@ -231,9 +231,9 @@
    10.4           or should I be using them somehow? *)
    10.5            fun mk_insts env =
    10.6              (Vartab.dest (Envir.type_env env),
    10.7 -             Envir.alist_of env);
    10.8 -          val initenv = Envir.Envir {asol = Vartab.empty,
    10.9 -                                     iTs = typinsttab, maxidx = ix2};
   10.10 +             Vartab.dest (Envir.term_env env));
   10.11 +          val initenv =
   10.12 +            Envir.Envir {maxidx = ix2, tenv = Vartab.empty, tyenv = typinsttab};
   10.13            val useq = Unify.smash_unifiers thry [a] initenv
   10.14  	            handle UnequalLengths => Seq.empty
   10.15  		               | Term.TERM _ => Seq.empty;
    11.1 --- a/src/Tools/induct.ML	Fri Jul 17 21:33:00 2009 +0200
    11.2 +++ b/src/Tools/induct.ML	Fri Jul 17 21:33:00 2009 +0200
    11.3 @@ -423,14 +423,15 @@
    11.4  
    11.5  local
    11.6  
    11.7 -fun dest_env thy (env as Envir.Envir {iTs, ...}) =
    11.8 +fun dest_env thy env =
    11.9    let
   11.10      val cert = Thm.cterm_of thy;
   11.11      val certT = Thm.ctyp_of thy;
   11.12 -    val pairs = Envir.alist_of env;
   11.13 +    val pairs = Vartab.dest (Envir.term_env env);
   11.14 +    val types = Vartab.dest (Envir.type_env env);
   11.15      val ts = map (cert o Envir.norm_term env o #2 o #2) pairs;
   11.16      val xs = map2 (curry (cert o Var)) (map #1 pairs) (map (#T o Thm.rep_cterm) ts);
   11.17 -  in (map (fn (xi, (S, T)) => (certT (TVar (xi, S)), certT T)) (Vartab.dest iTs), xs ~~ ts) end;
   11.18 +  in (map (fn (xi, (S, T)) => (certT (TVar (xi, S)), certT T)) types, xs ~~ ts) end;
   11.19  
   11.20  in
   11.21  
   11.22 @@ -450,8 +451,7 @@
   11.23          val rule' = Thm.incr_indexes (maxidx + 1) rule;
   11.24          val concl = Logic.strip_assums_concl goal;
   11.25        in
   11.26 -        Unify.smash_unifiers thy [(Thm.concl_of rule', concl)]
   11.27 -          (Envir.empty (#maxidx (Thm.rep_thm rule')))
   11.28 +        Unify.smash_unifiers thy [(Thm.concl_of rule', concl)] (Envir.empty (Thm.maxidx_of rule'))
   11.29          |> Seq.map (fn env => Drule.instantiate (dest_env thy env) rule')
   11.30        end
   11.31    end handle Subscript => Seq.empty;