# HG changeset patch
# User wenzelm
# Date 1247865237 -7200
# Node ID b3eaeb39da83fdedfaf490a987d31659a31e30fb
# Parent  c141f139ce26272b5b28396be7d4f2415e7de3ce# Parent  3b12e03e4178d710ba755a1a5ad7bc452daaa1e1
merged

diff -r c141f139ce26 -r b3eaeb39da83 src/HOL/Library/reflection.ML
--- a/src/HOL/Library/reflection.ML	Fri Jul 17 13:12:18 2009 -0400
+++ b/src/HOL/Library/reflection.ML	Fri Jul 17 23:13:57 2009 +0200
@@ -153,8 +153,8 @@
             val certy = ctyp_of thy
             val (tyenv, tmenv) =
               Pattern.match thy
-              ((fst o HOLogic.dest_eq o HOLogic.dest_Trueprop) (concl_of cong), t)
-              (Envir.type_env (Envir.empty 0), Vartab.empty)
+                ((fst o HOLogic.dest_eq o HOLogic.dest_Trueprop) (concl_of cong), t)
+                (Vartab.empty, Vartab.empty)
             val (fnvs,invs) = List.partition (fn ((vn,_),_) => vn mem vns) (Vartab.dest tmenv)
             val (fts,its) =
 	      (map (snd o snd) fnvs,
@@ -204,11 +204,9 @@
             val xns_map = (fst (split_list nths)) ~~ xns
             val subst = map (fn (nt, xn) => (nt, Var ((xn,0), fastype_of nt))) xns_map
             val rhs_P = subst_free subst rhs
-            val (tyenv, tmenv) = Pattern.match
-                              thy (rhs_P, t)
-                              (Envir.type_env (Envir.empty 0), Vartab.empty)
-            val sbst = Envir.subst_vars (tyenv, tmenv)
-            val sbsT = Envir.typ_subst_TVars tyenv
+            val (tyenv, tmenv) = Pattern.match thy (rhs_P, t) (Vartab.empty, Vartab.empty)
+            val sbst = Envir.subst_term (tyenv, tmenv)
+            val sbsT = Envir.subst_type tyenv
             val subst_ty = map (fn (n,(s,t)) => (certT (TVar (n, s)), certT t))
                                (Vartab.dest tyenv)
             val tml = Vartab.dest tmenv
diff -r c141f139ce26 -r b3eaeb39da83 src/HOL/Nominal/nominal_inductive.ML
--- a/src/HOL/Nominal/nominal_inductive.ML	Fri Jul 17 13:12:18 2009 -0400
+++ b/src/HOL/Nominal/nominal_inductive.ML	Fri Jul 17 23:13:57 2009 +0200
@@ -342,7 +342,7 @@
                  val env = Pattern.first_order_match thy (ihypt, prop_of ihyp)
                    (Vartab.empty, Vartab.empty);
                  val ihyp' = Thm.instantiate ([], map (pairself (cterm_of thy))
-                   (map (Envir.subst_vars env) vs ~~
+                   (map (Envir.subst_term env) vs ~~
                     map (fold_rev (NominalDatatype.mk_perm [])
                       (rev pis' @ pis)) params' @ [z])) ihyp;
                  fun mk_pi th =
diff -r c141f139ce26 -r b3eaeb39da83 src/HOL/Nominal/nominal_inductive2.ML
--- a/src/HOL/Nominal/nominal_inductive2.ML	Fri Jul 17 13:12:18 2009 -0400
+++ b/src/HOL/Nominal/nominal_inductive2.ML	Fri Jul 17 23:13:57 2009 +0200
@@ -147,7 +147,7 @@
   let val env = Pattern.first_order_match thy (p, prop_of th)
     (Vartab.empty, Vartab.empty)
   in Thm.instantiate ([],
-    map (Envir.subst_vars env #> cterm_of thy) vs ~~ cts) th
+    map (Envir.subst_term env #> cterm_of thy) vs ~~ cts) th
   end;
 
 fun prove_strong_ind s avoids ctxt =
diff -r c141f139ce26 -r b3eaeb39da83 src/HOL/Tools/Datatype/datatype_case.ML
--- a/src/HOL/Tools/Datatype/datatype_case.ML	Fri Jul 17 13:12:18 2009 -0400
+++ b/src/HOL/Tools/Datatype/datatype_case.ML	Fri Jul 17 23:13:57 2009 +0200
@@ -293,7 +293,7 @@
   end;
 
 fun make_case tab ctxt = gen_make_case
-  (match_type (ProofContext.theory_of ctxt)) Envir.subst_TVars fastype_of tab ctxt;
+  (match_type (ProofContext.theory_of ctxt)) Envir.subst_term_types fastype_of tab ctxt;
 val make_case_untyped = gen_make_case (K (K Vartab.empty))
   (K (Term.map_types (K dummyT))) (K dummyT);
 
diff -r c141f139ce26 -r b3eaeb39da83 src/HOL/Tools/Function/context_tree.ML
--- a/src/HOL/Tools/Function/context_tree.ML	Fri Jul 17 13:12:18 2009 -0400
+++ b/src/HOL/Tools/Function/context_tree.ML	Fri Jul 17 23:13:57 2009 +0200
@@ -116,8 +116,9 @@
        val (c, subs) = (concl_of r, prems_of r)
 
        val subst = Pattern.match (ProofContext.theory_of ctx) (c, tt') (Vartab.empty, Vartab.empty)
-       val branches = map (mk_branch ctx o Envir.beta_norm o Envir.subst_vars subst) subs
-       val inst = map (fn v => (cterm_of thy (Var v), cterm_of thy (Envir.subst_vars subst (Var v)))) (Term.add_vars c [])
+       val branches = map (mk_branch ctx o Envir.beta_norm o Envir.subst_term subst) subs
+       val inst = map (fn v =>
+        (cterm_of thy (Var v), cterm_of thy (Envir.subst_term subst (Var v)))) (Term.add_vars c [])
      in
    (cterm_instantiate inst r, dep, branches)
      end
diff -r c141f139ce26 -r b3eaeb39da83 src/HOL/Tools/Function/fundef_datatype.ML
--- a/src/HOL/Tools/Function/fundef_datatype.ML	Fri Jul 17 13:12:18 2009 -0400
+++ b/src/HOL/Tools/Function/fundef_datatype.ML	Fri Jul 17 23:13:57 2009 +0200
@@ -102,7 +102,8 @@
 
 
 fun inst_constrs_of thy (T as Type (name, _)) =
-        map (fn (Cn,CT) => Envir.subst_TVars (Sign.typ_match thy (body_type CT, T) Vartab.empty) (Const (Cn, CT)))
+        map (fn (Cn,CT) =>
+              Envir.subst_term_types (Sign.typ_match thy (body_type CT, T) Vartab.empty) (Const (Cn, CT)))
             (the (Datatype.get_constrs thy name))
   | inst_constrs_of thy _ = raise Match
 
diff -r c141f139ce26 -r b3eaeb39da83 src/HOL/Tools/Function/mutual.ML
--- a/src/HOL/Tools/Function/mutual.ML	Fri Jul 17 13:12:18 2009 -0400
+++ b/src/HOL/Tools/Function/mutual.ML	Fri Jul 17 23:13:57 2009 +0200
@@ -100,7 +100,7 @@
         val (caTss, resultTs) = split_list (map curried_types fs)
         val argTs = map (foldr1 HOLogic.mk_prodT) caTss
 
-        val dresultTs = distinct (Type.eq_type Vartab.empty) resultTs
+        val dresultTs = distinct (op =) resultTs
         val n' = length dresultTs
 
         val RST = BalancedTree.make (uncurry SumTree.mk_sumT) dresultTs
@@ -114,7 +114,7 @@
         fun define (fvar as (n, T)) caTs resultT i =
             let
                 val vars = map_index (fn (j,T) => Free ("x" ^ string_of_int j, T)) caTs (* FIXME: Bind xs properly *)
-                val i' = find_index (fn Ta => Type.eq_type Vartab.empty (Ta, resultT)) dresultTs + 1 
+                val i' = find_index (fn Ta => Ta = resultT) dresultTs + 1 
 
                 val f_exp = SumTree.mk_proj RST n' i' (Free fsum_var $ SumTree.mk_inj ST num i (foldr1 HOLogic.mk_prod vars))
                 val def = Term.abstract_over (Free fsum_var, fold_rev lambda vars f_exp)
diff -r c141f139ce26 -r b3eaeb39da83 src/HOL/Tools/Function/pattern_split.ML
--- a/src/HOL/Tools/Function/pattern_split.ML	Fri Jul 17 13:12:18 2009 -0400
+++ b/src/HOL/Tools/Function/pattern_split.ML	Fri Jul 17 23:13:57 2009 +0200
@@ -39,7 +39,8 @@
          
 (* This is copied from "fundef_datatype.ML" *)
 fun inst_constrs_of thy (T as Type (name, _)) =
-    map (fn (Cn,CT) => Envir.subst_TVars (Sign.typ_match thy (body_type CT, T) Vartab.empty) (Const (Cn, CT)))
+    map (fn (Cn,CT) =>
+          Envir.subst_term_types (Sign.typ_match thy (body_type CT, T) Vartab.empty) (Const (Cn, CT)))
         (the (Datatype.get_constrs thy name))
   | inst_constrs_of thy T = raise TYPE ("inst_constrs_of", [T], [])
                             
diff -r c141f139ce26 -r b3eaeb39da83 src/HOL/Tools/TFL/casesplit.ML
--- a/src/HOL/Tools/TFL/casesplit.ML	Fri Jul 17 13:12:18 2009 -0400
+++ b/src/HOL/Tools/TFL/casesplit.ML	Fri Jul 17 23:13:57 2009 +0200
@@ -129,8 +129,8 @@
           | _ => error "not a valid case thm";
       val type_cinsts = map (fn (ixn, (S, T)) => (ctypify (TVar (ixn, S)), ctypify T))
         (Vartab.dest type_insts);
-      val cPv = ctermify (Envir.subst_TVars type_insts Pv);
-      val cDv = ctermify (Envir.subst_TVars type_insts Dv);
+      val cPv = ctermify (Envir.subst_term_types type_insts Pv);
+      val cDv = ctermify (Envir.subst_term_types type_insts Dv);
     in
       (beta_eta_contract
          (case_thm
diff -r c141f139ce26 -r b3eaeb39da83 src/HOL/Tools/TFL/thry.ML
--- a/src/HOL/Tools/TFL/thry.ML	Fri Jul 17 13:12:18 2009 -0400
+++ b/src/HOL/Tools/TFL/thry.ML	Fri Jul 17 23:13:57 2009 +0200
@@ -35,7 +35,7 @@
 fun match_term thry pat ob =
   let
     val (ty_theta, tm_theta) = Pattern.match thry (pat,ob) (Vartab.empty, Vartab.empty);
-    fun tmbind (ixn, (T, t)) = (Var (ixn, Envir.typ_subst_TVars ty_theta T), t)
+    fun tmbind (ixn, (T, t)) = (Var (ixn, Envir.subst_type ty_theta T), t)
   in (map tmbind (Vartab.dest tm_theta), map tybind (Vartab.dest ty_theta))
   end;
 
diff -r c141f139ce26 -r b3eaeb39da83 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Fri Jul 17 13:12:18 2009 -0400
+++ b/src/HOL/Tools/inductive.ML	Fri Jul 17 23:13:57 2009 +0200
@@ -922,7 +922,7 @@
         val tab = fold (Pattern.first_order_match thy) (ts ~~ us)
           (Vartab.empty, Vartab.empty);
       in
-        map (Envir.subst_vars tab) vars
+        map (Envir.subst_term tab) vars
       end
   in
     map (mtch o apsnd prop_of) (cases ~~ intros)
diff -r c141f139ce26 -r b3eaeb39da83 src/HOL/Tools/inductive_set.ML
--- a/src/HOL/Tools/inductive_set.ML	Fri Jul 17 13:12:18 2009 -0400
+++ b/src/HOL/Tools/inductive_set.ML	Fri Jul 17 23:13:57 2009 +0200
@@ -324,7 +324,7 @@
 fun to_pred_proc thy rules t = case lookup_rule thy I rules t of
     NONE => NONE
   | SOME (lhs, rhs) =>
-      SOME (Envir.subst_vars
+      SOME (Envir.subst_term
         (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) rhs);
 
 fun to_pred thms ctxt thm =
diff -r c141f139ce26 -r b3eaeb39da83 src/HOL/Tools/meson.ML
--- a/src/HOL/Tools/meson.ML	Fri Jul 17 13:12:18 2009 -0400
+++ b/src/HOL/Tools/meson.ML	Fri Jul 17 23:13:57 2009 +0200
@@ -87,14 +87,12 @@
 fun typ_pair_of (ix, (sort,ty)) = (TVar (ix,sort), ty);
 fun term_pair_of (ix, (ty,t)) = (Var (ix,ty), t);
 
-val Envir.Envir {asol = tenv0, iTs = tyenv0, ...} = Envir.empty 0
-
 (*FIXME: currently does not "rename variables apart"*)
 fun first_order_resolve thA thB =
   let val thy = theory_of_thm thA
       val tmA = concl_of thA
       val Const("==>",_) $ tmB $ _ = prop_of thB
-      val (tyenv,tenv) = Pattern.first_order_match thy (tmB,tmA) (tyenv0,tenv0)
+      val (tyenv, tenv) = Pattern.first_order_match thy (tmB, tmA) (Vartab.empty, Vartab.empty)
       val ct_pairs = map (pairself (cterm_of thy) o term_pair_of) (Vartab.dest tenv)
   in  thA RS (cterm_instantiate ct_pairs thB)  end
   handle _ => raise THM ("first_order_resolve", 0, [thA,thB]);  (* FIXME avoid handle _ *)
@@ -104,8 +102,8 @@
       [] => th
     | pairs =>
         let val thy = theory_of_thm th
-            val (tyenv,tenv) =
-                  List.foldl (uncurry (Pattern.first_order_match thy)) (tyenv0,tenv0) pairs
+            val (tyenv, tenv) =
+              fold (Pattern.first_order_match thy) pairs (Vartab.empty, Vartab.empty)
             val t_pairs = map term_pair_of (Vartab.dest tenv)
             val th' = Thm.instantiate ([], map (pairself (cterm_of thy)) t_pairs) th
         in  th'  end
diff -r c141f139ce26 -r b3eaeb39da83 src/HOLCF/Tools/adm_tac.ML
--- a/src/HOLCF/Tools/adm_tac.ML	Fri Jul 17 13:12:18 2009 -0400
+++ b/src/HOLCF/Tools/adm_tac.ML	Fri Jul 17 23:13:57 2009 +0200
@@ -117,8 +117,8 @@
     val tye' = Sign.typ_match thy (PT, #T (rep_cterm Pt)) tye;
     val ctye = map (fn (ixn, (S, T)) =>
       (ctyp_of thy (TVar (ixn, S)), ctyp_of thy T)) (Vartab.dest tye');
-    val tv = cterm_of thy (Var (("t", j), Envir.typ_subst_TVars tye' tT));
-    val Pv = cterm_of thy (Var (("P", j), Envir.typ_subst_TVars tye' PT));
+    val tv = cterm_of thy (Var (("t", j), Envir.subst_type tye' tT));
+    val Pv = cterm_of thy (Var (("P", j), Envir.subst_type tye' PT));
     val rule' = instantiate (ctye, [(tv, tt), (Pv, Pt)]) rule
   in rule' end;
 
diff -r c141f139ce26 -r b3eaeb39da83 src/Pure/Isar/overloading.ML
--- a/src/Pure/Isar/overloading.ML	Fri Jul 17 13:12:18 2009 -0400
+++ b/src/Pure/Isar/overloading.ML	Fri Jul 17 23:13:57 2009 +0200
@@ -76,7 +76,7 @@
           | _ => I)
       | accumulate_improvements _ = I;
     val improvements = (fold o fold_aterms) accumulate_improvements ts Vartab.empty;
-    val ts' = (map o map_types) (Envir.typ_subst_TVars improvements) ts;
+    val ts' = (map o map_types) (Envir.subst_type improvements) ts;
     fun apply_subst t = Envir.expand_term (fn Const (c, ty) => (case subst (c, ty)
          of SOME (ty', t') =>
               if Type.typ_instance tsig (ty, ty')
diff -r c141f139ce26 -r b3eaeb39da83 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Fri Jul 17 13:12:18 2009 -0400
+++ b/src/Pure/Isar/proof_context.ML	Fri Jul 17 23:13:57 2009 +0200
@@ -779,7 +779,7 @@
 fun simult_matches ctxt (t, pats) =
   (case Seq.pull (Unify.matchers (theory_of ctxt) (map (rpair t) pats)) of
     NONE => error "Pattern match failed!"
-  | SOME (env, _) => map (apsnd snd) (Envir.alist_of env));
+  | SOME (env, _) => Vartab.fold (fn (v, (_, t)) => cons (v, t)) (Envir.term_env env) []);
 
 
 (* bind_terms *)
diff -r c141f139ce26 -r b3eaeb39da83 src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Fri Jul 17 13:12:18 2009 -0400
+++ b/src/Pure/Proof/extraction.ML	Fri Jul 17 23:13:57 2009 +0200
@@ -103,11 +103,10 @@
           fun ren t = the_default t (Term.rename_abs tm1 tm t);
           val inc = Logic.incr_indexes ([], maxidx_of_term tm + 1);
           val env as (Tenv, tenv) = Pattern.match thy (inc tm1, tm) (Vartab.empty, Vartab.empty);
-          val prems' = map (pairself (Envir.subst_vars env o inc o ren)) prems;
+          val prems' = map (pairself (Envir.subst_term env o inc o ren)) prems;
           val env' = Envir.Envir
-            {maxidx = Library.foldl Int.max
-              (~1, map (Int.max o pairself maxidx_of_term) prems'),
-             iTs = Tenv, asol = tenv};
+            {maxidx = fold (fn (t, u) => Term.maxidx_term t #> Term.maxidx_term u) prems' ~1,
+             tenv = tenv, tyenv = Tenv};
           val env'' = fold (Pattern.unify thy o pairself (lookup rew)) prems' env';
         in SOME (Envir.norm_term env'' (inc (ren tm2)))
         end handle Pattern.MATCH => NONE | Pattern.Unif => NONE)
diff -r c141f139ce26 -r b3eaeb39da83 src/Pure/Proof/reconstruct.ML
--- a/src/Pure/Proof/reconstruct.ML	Fri Jul 17 13:12:18 2009 -0400
+++ b/src/Pure/Proof/reconstruct.ML	Fri Jul 17 23:13:57 2009 +0200
@@ -35,12 +35,6 @@
 fun forall_intr_vfs_prf prop prf = fold_rev forall_intr_prf
   (vars_of prop @ frees_of prop) prf;
 
-fun merge_envs (Envir.Envir {asol=asol1, iTs=iTs1, maxidx=maxidx1})
-  (Envir.Envir {asol=asol2, iTs=iTs2, maxidx=maxidx2}) =
-    Envir.Envir {asol=Vartab.merge (op =) (asol1, asol2),
-                 iTs=Vartab.merge (op =) (iTs1, iTs2),
-                 maxidx=Int.max (maxidx1, maxidx2)};
-
 
 (**** generate constraints for proof term ****)
 
@@ -48,31 +42,32 @@
   let val (env', v) = Envir.genvar "a" (env, rev Ts ---> T)
   in (env', list_comb (v, map Bound (length Ts - 1 downto 0))) end;
 
-fun mk_tvar (Envir.Envir {iTs, asol, maxidx}, s) =
-  (Envir.Envir {iTs = iTs, asol = asol, maxidx = maxidx+1},
-   TVar (("'t", maxidx+1), s));
+fun mk_tvar (Envir.Envir {maxidx, tenv, tyenv}, s) =
+  (Envir.Envir {maxidx = maxidx + 1, tenv = tenv, tyenv = tyenv},
+   TVar (("'t", maxidx + 1), s));
 
 val mk_abs = fold (fn T => fn u => Abs ("", T, u));
 
 fun unifyT thy env T U =
   let
-    val Envir.Envir {asol, iTs, maxidx} = env;
-    val (iTs', maxidx') = Sign.typ_unify thy (T, U) (iTs, maxidx)
-  in Envir.Envir {asol=asol, iTs=iTs', maxidx=maxidx'} end
-  handle Type.TUNIFY => error ("Non-unifiable types:\n" ^
-    Syntax.string_of_typ_global thy T ^ "\n\n" ^ Syntax.string_of_typ_global thy U);
+    val Envir.Envir {maxidx, tenv, tyenv} = env;
+    val (tyenv', maxidx') = Sign.typ_unify thy (T, U) (tyenv, maxidx);
+  in Envir.Envir {maxidx = maxidx', tenv = tenv, tyenv = tyenv'} end;
 
-fun chaseT (env as Envir.Envir {iTs, ...}) (T as TVar ixnS) =
-      (case Type.lookup iTs ixnS of NONE => T | SOME T' => chaseT env T')
+fun chaseT env (T as TVar v) =
+      (case Type.lookup (Envir.type_env env) v of
+        NONE => T
+      | SOME T' => chaseT env T')
   | chaseT _ T = T;
 
-fun infer_type thy (env as Envir.Envir {maxidx, asol, iTs}) Ts vTs
-      (t as Const (s, T)) = if T = dummyT then (case Sign.const_type thy s of
+fun infer_type thy (env as Envir.Envir {maxidx, tenv, tyenv}) Ts vTs
+      (t as Const (s, T)) = if T = dummyT then
+        (case Sign.const_type thy s of
           NONE => error ("reconstruct_proof: No such constant: " ^ quote s)
         | SOME T =>
             let val T' = Type.strip_sorts (Logic.incr_tvar (maxidx + 1) T)
             in (Const (s, T'), T', vTs,
-              Envir.Envir {maxidx = maxidx + 1, asol = asol, iTs = iTs})
+              Envir.Envir {maxidx = maxidx + 1, tenv = tenv, tyenv = tyenv})
             end)
       else (t, T, vTs, env)
   | infer_type thy env Ts vTs (t as Free (s, T)) =
@@ -236,21 +231,23 @@
 
 fun upd_constrs env cs =
   let
-    val Envir.Envir {asol, iTs, ...} = env;
+    val tenv = Envir.term_env env;
+    val tyenv = Envir.type_env env;
     val dom = []
-      |> Vartab.fold (cons o #1) asol
-      |> Vartab.fold (cons o #1) iTs;
+      |> Vartab.fold (cons o #1) tenv
+      |> Vartab.fold (cons o #1) tyenv;
     val vran = []
-      |> Vartab.fold (Term.add_var_names o #2 o #2) asol
-      |> Vartab.fold (Term.add_tvar_namesT o #2 o #2) iTs;
+      |> Vartab.fold (Term.add_var_names o #2 o #2) tenv
+      |> Vartab.fold (Term.add_tvar_namesT o #2 o #2) tyenv;
     fun check_cs [] = []
-      | check_cs ((u, p, vs)::ps) =
-          let val vs' = subtract (op =) dom vs;
-          in if vs = vs' then (u, p, vs)::check_cs ps
-             else (true, p, fold (insert (op =)) vs' vran)::check_cs ps
-          end
+      | check_cs ((u, p, vs) :: ps) =
+          let val vs' = subtract (op =) dom vs in
+            if vs = vs' then (u, p, vs) :: check_cs ps
+            else (true, p, fold (insert op =) vs' vran) :: check_cs ps
+          end;
   in check_cs cs end;
 
+
 (**** solution of constraints ****)
 
 fun solve _ [] bigenv = bigenv
@@ -280,7 +277,7 @@
         val Envir.Envir {maxidx, ...} = bigenv;
         val (env, cs') = search (Envir.empty maxidx) cs;
       in
-        solve thy (upd_constrs env cs') (merge_envs bigenv env)
+        solve thy (upd_constrs env cs') (Envir.merge (bigenv, env))
       end;
 
 
diff -r c141f139ce26 -r b3eaeb39da83 src/Pure/defs.ML
--- a/src/Pure/defs.ML	Fri Jul 17 13:12:18 2009 -0400
+++ b/src/Pure/defs.ML	Fri Jul 17 23:13:57 2009 +0200
@@ -46,7 +46,7 @@
       handle Type.TUNIFY => true);
 
 fun match_args (Ts, Us) =
-  Option.map Envir.typ_subst_TVars
+  Option.map Envir.subst_type
     (SOME (Type.raw_matches (Ts, Us) Vartab.empty) handle Type.TYPE_MATCH => NONE);
 
 
diff -r c141f139ce26 -r b3eaeb39da83 src/Pure/envir.ML
--- a/src/Pure/envir.ML	Fri Jul 17 13:12:18 2009 -0400
+++ b/src/Pure/envir.ML	Fri Jul 17 23:13:57 2009 +0200
@@ -1,27 +1,29 @@
 (*  Title:      Pure/envir.ML
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
 
-Environments.  The type of a term variable / sort of a type variable is
-part of its name. The lookup function must apply type substitutions,
+Free-form environments.  The type of a term variable / sort of a type variable is
+part of its name.  The lookup function must apply type substitutions,
 since they may change the identity of a variable.
 *)
 
 signature ENVIR =
 sig
   type tenv = (typ * term) Vartab.table
-  datatype env = Envir of {asol: tenv, iTs: Type.tyenv, maxidx: int}
+  datatype env = Envir of {maxidx: int, tenv: tenv, tyenv: Type.tyenv}
+  val maxidx_of: env -> int
+  val term_env: env -> tenv
   val type_env: env -> Type.tyenv
+  val is_empty: env -> bool
+  val empty: int -> env
+  val merge: env * env -> env
   val insert_sorts: env -> sort list -> sort list
   val genvars: string -> env * typ list -> env * term list
   val genvar: string -> env * typ -> env * term
   val lookup: env * (indexname * typ) -> term option
   val lookup': tenv * (indexname * typ) -> term option
   val update: ((indexname * typ) * term) * env -> env
-  val empty: int -> env
-  val is_empty: env -> bool
   val above: env -> int -> bool
   val vupdate: ((indexname * typ) * term) * env -> env
-  val alist_of: env -> (indexname * (typ * term)) list
   val norm_type_same: Type.tyenv -> typ Same.operation
   val norm_types_same: Type.tyenv -> typ list Same.operation
   val norm_type: Type.tyenv -> typ -> typ
@@ -32,124 +34,144 @@
   val eta_contract: term -> term
   val beta_eta_contract: term -> term
   val fastype: env -> typ list -> term -> typ
-  val typ_subst_TVars: Type.tyenv -> typ -> typ
-  val subst_TVars: Type.tyenv -> term -> term
-  val subst_Vars: tenv -> term -> term
-  val subst_vars: Type.tyenv * tenv -> term -> term
+  val subst_type_same: Type.tyenv -> typ Same.operation
+  val subst_term_types_same: Type.tyenv -> term Same.operation
+  val subst_term_same: Type.tyenv * tenv -> term Same.operation
+  val subst_type: Type.tyenv -> typ -> typ
+  val subst_term_types: Type.tyenv -> term -> term
+  val subst_term: Type.tyenv * tenv -> term -> term
   val expand_atom: typ -> typ * term -> term
   val expand_term: (term -> (typ * term) option) -> term -> term
   val expand_term_frees: ((string * typ) * term) list -> term -> term
 end;
 
-structure Envir : ENVIR =
+structure Envir: ENVIR =
 struct
 
-(*updating can destroy environment in 2 ways!!
-   (1) variables out of range   (2) circular assignments
+(** datatype env **)
+
+(*Updating can destroy environment in 2 ways!
+   (1) variables out of range
+   (2) circular assignments
 *)
+
 type tenv = (typ * term) Vartab.table;
 
 datatype env = Envir of
- {maxidx: int,      (*maximum index of vars*)
-  asol: tenv,       (*assignments to Vars*)
-  iTs: Type.tyenv}; (*assignments to TVars*)
+ {maxidx: int,          (*upper bound of maximum index of vars*)
+  tenv: tenv,           (*assignments to Vars*)
+  tyenv: Type.tyenv};   (*assignments to TVars*)
+
+fun make_env (maxidx, tenv, tyenv) = Envir {maxidx = maxidx, tenv = tenv, tyenv = tyenv};
+fun map_env f (Envir {maxidx, tenv, tyenv}) = make_env (f (maxidx, tenv, tyenv));
+
+fun maxidx_of (Envir {maxidx, ...}) = maxidx;
+fun term_env (Envir {tenv, ...}) = tenv;
+fun type_env (Envir {tyenv, ...}) = tyenv;
+
+fun is_empty env =
+  Vartab.is_empty (term_env env) andalso
+  Vartab.is_empty (type_env env);
 
-fun type_env (Envir {iTs, ...}) = iTs;
+
+(* build env *)
+
+fun empty maxidx = make_env (maxidx, Vartab.empty, Vartab.empty);
 
-(*NB: type unification may invent new sorts*)
+fun merge
+   (Envir {maxidx = maxidx1, tenv = tenv1, tyenv = tyenv1},
+    Envir {maxidx = maxidx2, tenv = tenv2, tyenv = tyenv2}) =
+  make_env (Int.max (maxidx1, maxidx2),
+    Vartab.merge (op =) (tenv1, tenv2),
+    Vartab.merge (op =) (tyenv1, tyenv2));
+
+
+(*NB: type unification may invent new sorts*)  (* FIXME tenv!? *)
 val insert_sorts = Vartab.fold (fn (_, (_, T)) => Sorts.insert_typ T) o type_env;
 
 (*Generate a list of distinct variables.
   Increments index to make them distinct from ALL present variables. *)
-fun genvars name (Envir{maxidx, asol, iTs}, Ts) : env * term list =
+fun genvars name (Envir {maxidx, tenv, tyenv}, Ts) : env * term list =
   let
     fun genvs (_, [] : typ list) : term list = []
       | genvs (n, [T]) = [Var ((name, maxidx + 1), T)]
       | genvs (n, T :: Ts) =
           Var ((name ^ radixstring (26, "a" , n), maxidx + 1), T)
             :: genvs (n + 1, Ts);
-  in (Envir {maxidx = maxidx + 1, asol = asol, iTs = iTs}, genvs (0, Ts)) end;
+  in (Envir {maxidx = maxidx + 1, tenv = tenv, tyenv = tyenv}, genvs (0, Ts)) end;
 
 (*Generate a variable.*)
 fun genvar name (env, T) : env * term =
   let val (env', [v]) = genvars name (env, [T])
   in (env', v) end;
 
-fun var_clash ixn T T' = raise TYPE ("Variable " ^
-    quote (Term.string_of_vname ixn) ^ " has two distinct types",
+fun var_clash xi T T' =
+  raise TYPE ("Variable " ^ quote (Term.string_of_vname xi) ^ " has two distinct types",
     [T', T], []);
 
-fun gen_lookup f asol (xname, T) =
-  (case Vartab.lookup asol xname of
+fun lookup_check check tenv (xi, T) =
+  (case Vartab.lookup tenv xi of
     NONE => NONE
-  | SOME (U, t) => if f (T, U) then SOME t else var_clash xname T U);
+  | SOME (U, t) => if check (T, U) then SOME t else var_clash xi T U);
 
 (* When dealing with environments produced by matching instead *)
 (* of unification, there is no need to chase assigned TVars.   *)
 (* In this case, we can simply ignore the type substitution    *)
 (* and use = instead of eq_type.                               *)
 
-fun lookup' (asol, p) = gen_lookup op = asol p;
+fun lookup' (tenv, p) = lookup_check (op =) tenv p;
 
-fun lookup2 (iTs, asol) p =
-  if Vartab.is_empty iTs then lookup' (asol, p)
-  else gen_lookup (Type.eq_type iTs) asol p;
-
-fun lookup (Envir {asol, iTs, ...}, p) = lookup2 (iTs, asol) p;
+fun lookup2 (tyenv, tenv) =
+  lookup_check (Type.eq_type tyenv) tenv;
 
-fun update (((xname, T), t), Envir {maxidx, asol, iTs}) =
-  Envir {maxidx = maxidx, asol = Vartab.update_new (xname, (T, t)) asol, iTs = iTs};
+fun lookup (Envir {tenv, tyenv, ...}, p) = lookup2 (tyenv, tenv) p;
 
-(*The empty environment.  New variables will start with the given index+1.*)
-fun empty m = Envir {maxidx = m, asol = Vartab.empty, iTs = Vartab.empty};
-
-(*Test for empty environment*)
-fun is_empty (Envir {asol, iTs, ...}) = Vartab.is_empty asol andalso Vartab.is_empty iTs;
+fun update (((xi, T), t), Envir {maxidx, tenv, tyenv}) =
+  Envir {maxidx = maxidx, tenv = Vartab.update_new (xi, (T, t)) tenv, tyenv = tyenv};
 
 (*Determine if the least index updated exceeds lim*)
-fun above (Envir {asol, iTs, ...}) lim =
-  (case Vartab.min_key asol of SOME (_, i) => i > lim | NONE => true) andalso
-  (case Vartab.min_key iTs of SOME (_, i) => i > lim | NONE => true);
+fun above (Envir {tenv, tyenv, ...}) lim =
+  (case Vartab.min_key tenv of SOME (_, i) => i > lim | NONE => true) andalso
+  (case Vartab.min_key tyenv of SOME (_, i) => i > lim | NONE => true);
 
 (*Update, checking Var-Var assignments: try to suppress higher indexes*)
-fun vupdate ((aU as (a, U), t), env as Envir {iTs, ...}) = case t of
-      Var (nT as (name', T)) =>
-        if a = name' then env     (*cycle!*)
-        else if TermOrd.indexname_ord (a, name') = LESS then
-           (case lookup (env, nT) of  (*if already assigned, chase*)
-                NONE => update ((nT, Var (a, T)), env)
-              | SOME u => vupdate ((aU, u), env))
-        else update ((aU, t), env)
-    | _ => update ((aU, t), env);
+fun vupdate ((aU as (a, U), t), env as Envir {tyenv, ...}) =
+  (case t of
+    Var (nT as (name', T)) =>
+      if a = name' then env     (*cycle!*)
+      else if TermOrd.indexname_ord (a, name') = LESS then
+        (case lookup (env, nT) of  (*if already assigned, chase*)
+          NONE => update ((nT, Var (a, T)), env)
+        | SOME u => vupdate ((aU, u), env))
+      else update ((aU, t), env)
+  | _ => update ((aU, t), env));
 
 
-(*Convert environment to alist*)
-fun alist_of (Envir{asol,...}) = Vartab.dest asol;
 
+(** beta normalization wrt. environment **)
 
-(*** Beta normal form for terms (not eta normal form).
-     Chases variables in env;  Does not exploit sharing of variable bindings
-     Does not check types, so could loop. ***)
+(*Chases variables in env.  Does not exploit sharing of variable bindings
+  Does not check types, so could loop.*)
 
 local
 
-fun norm_type0 iTs : typ Same.operation =
+fun norm_type0 tyenv : typ Same.operation =
   let
     fun norm (Type (a, Ts)) = Type (a, Same.map norm Ts)
       | norm (TFree _) = raise Same.SAME
       | norm (TVar v) =
-          (case Type.lookup iTs v of
+          (case Type.lookup tyenv v of
             SOME U => Same.commit norm U
           | NONE => raise Same.SAME);
   in norm end;
 
-fun norm_term1 asol : term Same.operation =
+fun norm_term1 tenv : term Same.operation =
   let
     fun norm (Var v) =
-          (case lookup' (asol, v) of
+          (case lookup' (tenv, v) of
             SOME u => Same.commit norm u
           | NONE => raise Same.SAME)
-      | norm (Abs (a, T, body)) =  Abs (a, T, norm body)
+      | norm (Abs (a, T, body)) = Abs (a, T, norm body)
       | norm (Abs (_, _, body) $ t) = Same.commit norm (subst_bound (t, body))
       | norm (f $ t) =
           ((case norm f of
@@ -159,13 +181,13 @@
       | norm _ = raise Same.SAME;
   in norm end;
 
-fun norm_term2 asol iTs : term Same.operation =
+fun norm_term2 tenv tyenv : term Same.operation =
   let
-    val normT = norm_type0 iTs;
+    val normT = norm_type0 tyenv;
     fun norm (Const (a, T)) = Const (a, normT T)
       | norm (Free (a, T)) = Free (a, normT T)
       | norm (Var (xi, T)) =
-          (case lookup2 (iTs, asol) (xi, T) of
+          (case lookup2 (tyenv, tenv) (xi, T) of
             SOME u => Same.commit norm u
           | NONE => Var (xi, normT T))
       | norm (Abs (a, T, body)) =
@@ -182,19 +204,19 @@
 
 in
 
-fun norm_type_same iTs T =
-  if Vartab.is_empty iTs then raise Same.SAME
-  else norm_type0 iTs T;
+fun norm_type_same tyenv T =
+  if Vartab.is_empty tyenv then raise Same.SAME
+  else norm_type0 tyenv T;
 
-fun norm_types_same iTs Ts =
-  if Vartab.is_empty iTs then raise Same.SAME
-  else Same.map (norm_type0 iTs) Ts;
+fun norm_types_same tyenv Ts =
+  if Vartab.is_empty tyenv then raise Same.SAME
+  else Same.map (norm_type0 tyenv) Ts;
 
-fun norm_type iTs T = norm_type_same iTs T handle Same.SAME => T;
+fun norm_type tyenv T = norm_type_same tyenv T handle Same.SAME => T;
 
-fun norm_term_same (Envir {asol, iTs, ...}) =
-  if Vartab.is_empty iTs then norm_term1 asol
-  else norm_term2 asol iTs;
+fun norm_term_same (Envir {tenv, tyenv, ...}) =
+  if Vartab.is_empty tyenv then norm_term1 tenv
+  else norm_term2 tenv tyenv;
 
 fun norm_term envir t = norm_term_same envir t handle Same.SAME => t;
 fun beta_norm t = if Term.has_abs t then norm_term (empty 0) t else t;
@@ -256,64 +278,89 @@
 
 (*finds type of term without checking that combinations are consistent
   Ts holds types of bound variables*)
-fun fastype (Envir {iTs, ...}) =
-let val funerr = "fastype: expected function type";
+fun fastype (Envir {tyenv, ...}) =
+  let
+    val funerr = "fastype: expected function type";
     fun fast Ts (f $ u) =
-        (case fast Ts f of
-           Type ("fun", [_, T]) => T
-         | TVar ixnS =>
-                (case Type.lookup iTs ixnS of
-                   SOME (Type ("fun", [_, T])) => T
-                 | _ => raise TERM (funerr, [f $ u]))
-         | _ => raise TERM (funerr, [f $ u]))
+          (case fast Ts f of
+            Type ("fun", [_, T]) => T
+          | TVar v =>
+              (case Type.lookup tyenv v of
+                SOME (Type ("fun", [_, T])) => T
+              | _ => raise TERM (funerr, [f $ u]))
+          | _ => raise TERM (funerr, [f $ u]))
       | fast Ts (Const (_, T)) = T
       | fast Ts (Free (_, T)) = T
       | fast Ts (Bound i) =
-        (nth Ts i
-         handle Subscript => raise TERM ("fastype: Bound", [Bound i]))
+          (nth Ts i handle Subscript => raise TERM ("fastype: Bound", [Bound i]))
       | fast Ts (Var (_, T)) = T
-      | fast Ts (Abs (_, T, u)) = T --> fast (T :: Ts) u
-in fast end;
+      | fast Ts (Abs (_, T, u)) = T --> fast (T :: Ts) u;
+  in fast end;
+
 
 
-(*Substitute for type Vars in a type*)
-fun typ_subst_TVars iTs T = if Vartab.is_empty iTs then T else
-  let fun subst(Type(a, Ts)) = Type(a, map subst Ts)
-        | subst(T as TFree _) = T
-        | subst(T as TVar ixnS) =
-            (case Type.lookup iTs ixnS of NONE => T | SOME(U) => U)
-  in subst T end;
+(** plain substitution -- without variable chasing **)
+
+local
 
-(*Substitute for type Vars in a term*)
-val subst_TVars = map_types o typ_subst_TVars;
+fun subst_type0 tyenv = Term_Subst.map_atypsT_same
+  (fn TVar v =>
+        (case Type.lookup tyenv v of
+          SOME U => U
+        | NONE => raise Same.SAME)
+    | _ => raise Same.SAME);
 
-(*Substitute for Vars in a term *)
-fun subst_Vars itms t = if Vartab.is_empty itms then t else
-  let fun subst (v as Var ixnT) = the_default v (lookup' (itms, ixnT))
-        | subst (Abs (a, T, t)) = Abs (a, T, subst t)
-        | subst (f $ t) = subst f $ subst t
-        | subst t = t
-  in subst t end;
+fun subst_term1 tenv = Term_Subst.map_aterms_same
+  (fn Var v =>
+        (case lookup' (tenv, v) of
+          SOME u => u
+        | NONE => raise Same.SAME)
+    | _ => raise Same.SAME);
 
-(*Substitute for type/term Vars in a term *)
-fun subst_vars (iTs, itms) =
-  if Vartab.is_empty iTs then subst_Vars itms else
-  let fun subst (Const (a, T)) = Const(a, typ_subst_TVars iTs T)
-        | subst (Free (a, T)) = Free (a, typ_subst_TVars iTs T)
-        | subst (Var (ixn, T)) = (case lookup' (itms, (ixn, T)) of
-            NONE   => Var (ixn, typ_subst_TVars iTs T)
-          | SOME t => t)
-        | subst (b as Bound _) = b
-        | subst (Abs (a, T, t)) = Abs(a, typ_subst_TVars iTs T, subst t)
-        | subst (f $ t) = subst f $ subst t
+fun subst_term2 tenv tyenv : term Same.operation =
+  let
+    val substT = subst_type0 tyenv;
+    fun subst (Const (a, T)) = Const (a, substT T)
+      | subst (Free (a, T)) = Free (a, substT T)
+      | subst (Var (xi, T)) =
+          (case lookup' (tenv, (xi, T)) of
+            SOME u => u
+          | NONE => Var (xi, substT T))
+      | subst (Bound _) = raise Same.SAME
+      | subst (Abs (a, T, t)) =
+          (Abs (a, substT T, Same.commit subst t)
+            handle Same.SAME => Abs (a, T, subst t))
+      | subst (t $ u) = (subst t $ Same.commit subst u handle Same.SAME => t $ subst u);
   in subst end;
 
+in
 
-(* expand defined atoms -- with local beta reduction *)
+fun subst_type_same tyenv T =
+  if Vartab.is_empty tyenv then raise Same.SAME
+  else subst_type0 tyenv T;
+
+fun subst_term_types_same tyenv t =
+  if Vartab.is_empty tyenv then raise Same.SAME
+  else Term_Subst.map_types_same (subst_type0 tyenv) t;
+
+fun subst_term_same (tyenv, tenv) =
+  if Vartab.is_empty tenv then subst_term_types_same tyenv
+  else if Vartab.is_empty tyenv then subst_term1 tenv
+  else subst_term2 tenv tyenv;
+
+fun subst_type tyenv T = subst_type_same tyenv T handle Same.SAME => T;
+fun subst_term_types tyenv t = subst_term_types_same tyenv t handle Same.SAME => t;
+fun subst_term envs t = subst_term_same envs t handle Same.SAME => t;
+
+end;
+
+
+
+(** expand defined atoms -- with local beta reduction **)
 
 fun expand_atom T (U, u) =
-  subst_TVars (Type.raw_match (U, T) Vartab.empty) u
-  handle Type.TYPE_MATCH => raise TYPE ("expand_atom: ill-typed replacement", [T, U], [u]);
+  subst_term_types (Type.raw_match (U, T) Vartab.empty) u
+    handle Type.TYPE_MATCH => raise TYPE ("expand_atom: ill-typed replacement", [T, U], [u]);
 
 fun expand_term get =
   let
@@ -326,10 +373,9 @@
         (case head of
           Abs (x, T, t) => comb (Abs (x, T, expand t))
         | _ =>
-            (case get head of
-              SOME def => Term.betapplys (expand_atom (Term.fastype_of head) def, args')
-            | NONE => comb head)
-        | _ => comb head)
+          (case get head of
+            SOME def => Term.betapplys (expand_atom (Term.fastype_of head) def, args')
+          | NONE => comb head))
       end;
   in expand end;
 
diff -r c141f139ce26 -r b3eaeb39da83 src/Pure/pattern.ML
--- a/src/Pure/pattern.ML	Fri Jul 17 13:12:18 2009 -0400
+++ b/src/Pure/pattern.ML	Fri Jul 17 23:13:57 2009 +0200
@@ -141,8 +141,10 @@
   | split_type (Type ("fun",[T1,T2]),n,Ts) = split_type (T2,n-1,T1::Ts)
   | split_type _                           = error("split_type");
 
-fun type_of_G (env as Envir.Envir {iTs, ...}) (T,n,is) =
-  let val (Ts, U) = split_type (Envir.norm_type iTs T, n, [])
+fun type_of_G env (T, n, is) =
+  let
+    val tyenv = Envir.type_env env;
+    val (Ts, U) = split_type (Envir.norm_type tyenv T, n, []);
   in map (nth Ts) is ---> U end;
 
 fun mkhnf (binders,is,G,js) = mkabs (binders, is, app(G,js));
@@ -225,11 +227,12 @@
                  end;
   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
 
-fun unify_types thy (T,U) (env as Envir.Envir{asol,iTs,maxidx}) =
-  if T=U then env
-  else let val (iTs',maxidx') = Sign.typ_unify thy (U, T) (iTs, maxidx)
-       in Envir.Envir{asol=asol,maxidx=maxidx',iTs=iTs'} end
-       handle Type.TUNIFY => (typ_clash thy (iTs,T,U); raise Unif);
+fun unify_types thy (T, U) (env as Envir.Envir {maxidx, tenv, tyenv}) =
+  if T = U then env
+  else
+    let val (tyenv', maxidx') = Sign.typ_unify thy (U, T) (tyenv, maxidx)
+    in Envir.Envir {maxidx = maxidx', tenv = tenv, tyenv = tyenv'} end
+    handle Type.TUNIFY => (typ_clash thy (tyenv, T, U); raise Unif);
 
 fun unif thy binders (s,t) env = case (Envir.head_norm env s, Envir.head_norm env t) of
       (Abs(ns,Ts,ts),Abs(nt,Tt,tt)) =>
@@ -351,7 +354,7 @@
       Abs(ns,Ts,ts) =>
         (case obj of
            Abs(nt,Tt,tt) => mtch ((nt,Tt)::binders) (ts,tt) env
-         | _ => let val Tt = Envir.typ_subst_TVars iTs Ts
+         | _ => let val Tt = Envir.subst_type iTs Ts
                 in mtch((ns,Tt)::binders) (ts,(incr obj)$Bound(0)) env end)
     | _ => (case obj of
               Abs(nt,Tt,tt) =>
@@ -425,7 +428,7 @@
 
 fun match_rew thy tm (tm1, tm2) =
   let val rtm = the_default tm2 (Term.rename_abs tm1 tm tm2) in
-    SOME (Envir.subst_vars (match thy (tm1, tm) (Vartab.empty, Vartab.empty)) rtm, rtm)
+    SOME (Envir.subst_term (match thy (tm1, tm) (Vartab.empty, Vartab.empty)) rtm, rtm)
       handle MATCH => NONE
   end;
 
diff -r c141f139ce26 -r b3eaeb39da83 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Fri Jul 17 13:12:18 2009 -0400
+++ b/src/Pure/proofterm.ML	Fri Jul 17 23:13:57 2009 +0200
@@ -489,9 +489,8 @@
   | remove_types (Const (s, _)) = Const (s, dummyT)
   | remove_types t = t;
 
-fun remove_types_env (Envir.Envir {iTs, asol, maxidx}) =
-  Envir.Envir {iTs = iTs, asol = Vartab.map (apsnd remove_types) asol,
-    maxidx = maxidx};
+fun remove_types_env (Envir.Envir {maxidx, tenv, tyenv}) =
+  Envir.Envir {maxidx = maxidx, tenv = Vartab.map (apsnd remove_types) tenv, tyenv = tyenv};
 
 fun norm_proof' env prf = norm_proof (remove_types_env env) prf;
 
@@ -1088,7 +1087,7 @@
 
 fun prf_subst (pinst, (tyinsts, insts)) =
   let
-    val substT = Envir.typ_subst_TVars tyinsts;
+    val substT = Envir.subst_type tyinsts;
 
     fun subst' lev (t as Var (ixn, _)) = (case AList.lookup (op =) insts ixn of
           NONE => t
diff -r c141f139ce26 -r b3eaeb39da83 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Fri Jul 17 13:12:18 2009 -0400
+++ b/src/Pure/thm.ML	Fri Jul 17 23:13:57 2009 +0200
@@ -317,7 +317,7 @@
       (Ctyp {T = TVar ((a, i), S), thy_ref = Theory.check_thy thy, maxidx = i, sorts = sorts},
        Ctyp {T = T, thy_ref = Theory.check_thy thy, maxidx = maxidx2, sorts = sorts});
     fun mk_ctinst ((x, i), (T, t)) =
-      let val T = Envir.typ_subst_TVars Tinsts T in
+      let val T = Envir.subst_type Tinsts T in
         (Cterm {t = Var ((x, i), T), T = T, thy_ref = Theory.check_thy thy,
           maxidx = i, sorts = sorts},
          Cterm {t = t, T = T, thy_ref = Theory.check_thy thy, maxidx = maxidx2, sorts = sorts})
@@ -1247,12 +1247,12 @@
     val Thm (der, {thy_ref, maxidx, shyps, hyps, prop, ...}) = state;
     val thy = Theory.deref thy_ref;
     val (tpairs, Bs, Bi, C) = dest_state (state, i);
-    fun newth n (env as Envir.Envir {maxidx, ...}, tpairs) =
+    fun newth n (env, tpairs) =
       Thm (deriv_rule1
           ((if Envir.is_empty env then I else (Pt.norm_proof' env)) o
             Pt.assumption_proof Bs Bi n) der,
        {tags = [],
-        maxidx = maxidx,
+        maxidx = Envir.maxidx_of env,
         shyps = Envir.insert_sorts env shyps,
         hyps = hyps,
         tpairs =
@@ -1465,15 +1465,15 @@
 
 (*Faster normalization: skip assumptions that were lifted over*)
 fun norm_term_skip env 0 t = Envir.norm_term env t
-  | norm_term_skip env n (Const("all",_)$Abs(a,T,t)) =
-        let val Envir.Envir{iTs, ...} = env
-            val T' = Envir.typ_subst_TVars iTs T
-            (*Must instantiate types of parameters because they are flattened;
-              this could be a NEW parameter*)
-        in Term.all T' $ Abs(a, T', norm_term_skip env n t)  end
-  | norm_term_skip env n (Const("==>", _) $ A $ B) =
-        Logic.mk_implies (A, norm_term_skip env (n-1) B)
-  | norm_term_skip env n t = error"norm_term_skip: too few assumptions??";
+  | norm_term_skip env n (Const ("all", _) $ Abs (a, T, t)) =
+      let
+        val T' = Envir.subst_type (Envir.type_env env) T
+        (*Must instantiate types of parameters because they are flattened;
+          this could be a NEW parameter*)
+      in Term.all T' $ Abs (a, T', norm_term_skip env n t) end
+  | norm_term_skip env n (Const ("==>", _) $ A $ B) =
+      Logic.mk_implies (A, norm_term_skip env (n - 1) B)
+  | norm_term_skip env n t = error "norm_term_skip: too few assumptions??";
 
 
 (*Composition of object rule r=(A1...Am/B) with proof state s=(B1...Bn/C)
@@ -1495,7 +1495,7 @@
      and nlift = Logic.count_prems (strip_all_body Bi) + (if eres_flg then ~1 else 0)
      val thy = Theory.deref (merge_thys2 state orule);
      (** Add new theorem with prop = '[| Bs; As |] ==> C' to thq **)
-     fun addth A (As, oldAs, rder', n) ((env as Envir.Envir {maxidx, ...}, tpairs), thq) =
+     fun addth A (As, oldAs, rder', n) ((env, tpairs), thq) =
        let val normt = Envir.norm_term env;
            (*perform minimal copying here by examining env*)
            val (ntpairs, normp) =
@@ -1520,7 +1520,7 @@
                        curry op oo (Pt.norm_proof' env))
                     (Pt.bicompose_proof flatten Bs oldAs As A n (nlift+1))) rder' sder,
                 {tags = [],
-                 maxidx = maxidx,
+                 maxidx = Envir.maxidx_of env,
                  shyps = Envir.insert_sorts env (Sorts.union rshyps sshyps),
                  hyps = union_hyps rhyps shyps,
                  tpairs = ntpairs,
diff -r c141f139ce26 -r b3eaeb39da83 src/Pure/type.ML
--- a/src/Pure/type.ML	Fri Jul 17 13:12:18 2009 -0400
+++ b/src/Pure/type.ML	Fri Jul 17 23:13:57 2009 +0200
@@ -494,12 +494,15 @@
 
 
 (*equality with respect to a type environment*)
-fun eq_type tye (T, T') =
+fun equal_type tye (T, T') =
   (case (devar tye T, devar tye T') of
      (Type (s, Ts), Type (s', Ts')) =>
-       s = s' andalso ListPair.all (eq_type tye) (Ts, Ts')
+       s = s' andalso ListPair.all (equal_type tye) (Ts, Ts')
    | (U, U') => U = U');
 
+fun eq_type tye =
+  if Vartab.is_empty tye then op = else equal_type tye;
+
 
 
 (** extend and merge type signatures **)
diff -r c141f139ce26 -r b3eaeb39da83 src/Pure/type_infer.ML
--- a/src/Pure/type_infer.ML	Fri Jul 17 13:12:18 2009 -0400
+++ b/src/Pure/type_infer.ML	Fri Jul 17 23:13:57 2009 +0200
@@ -402,7 +402,7 @@
 
     (*convert to preterms*)
     val ts = burrow_types check_typs raw_ts;
-    val (ts', (vps, ps)) =
+    val (ts', _) =
       fold_map (preterm_of const_type is_param o constrain_vars) ts (Vartab.empty, Vartab.empty);
 
     (*do type inference*)
diff -r c141f139ce26 -r b3eaeb39da83 src/Pure/unify.ML
--- a/src/Pure/unify.ML	Fri Jul 17 13:12:18 2009 -0400
+++ b/src/Pure/unify.ML	Fri Jul 17 23:13:57 2009 +0200
@@ -52,36 +52,48 @@
 
 type dpair = binderlist * term * term;
 
-fun body_type(Envir.Envir{iTs,...}) =
-let fun bT(Type("fun",[_,T])) = bT T
-      | bT(T as TVar ixnS) = (case Type.lookup iTs ixnS of
-    NONE => T | SOME(T') => bT T')
-      | bT T = T
-in bT end;
+fun body_type env =
+  let
+    val tyenv = Envir.type_env env;
+    fun bT (Type ("fun", [_, T])) = bT T
+      | bT (T as TVar v) =
+          (case Type.lookup tyenv v of
+            NONE => T
+          | SOME T' => bT T')
+      | bT T = T;
+  in bT end;
 
-fun binder_types(Envir.Envir{iTs,...}) =
-let fun bTs(Type("fun",[T,U])) = T :: bTs U
-      | bTs(T as TVar ixnS) = (case Type.lookup iTs ixnS of
-    NONE => [] | SOME(T') => bTs T')
-      | bTs _ = []
-in bTs end;
+fun binder_types env =
+  let
+    val tyenv = Envir.type_env env;
+    fun bTs (Type ("fun", [T, U])) = T :: bTs U
+      | bTs (T as TVar v) =
+          (case Type.lookup tyenv v of
+            NONE => []
+          | SOME T' => bTs T')
+      | bTs _ = [];
+  in bTs end;
 
 fun strip_type env T = (binder_types env T, body_type env T);
 
 fun fastype env (Ts, t) = Envir.fastype env (map snd Ts) t;
 
 
-(*Eta normal form*)
-fun eta_norm(env as Envir.Envir{iTs,...}) =
-  let fun etif (Type("fun",[T,U]), t) =
-      Abs("", T, etif(U, incr_boundvars 1 t $ Bound 0))
-  | etif (TVar ixnS, t) =
-      (case Type.lookup iTs ixnS of
-      NONE => t | SOME(T) => etif(T,t))
-  | etif (_,t) = t;
-      fun eta_nm (rbinder, Abs(a,T,body)) =
-      Abs(a, T, eta_nm ((a,T)::rbinder, body))
-  | eta_nm (rbinder, t) = etif(fastype env (rbinder,t), t)
+(* eta normal form *)
+
+fun eta_norm env =
+  let
+    val tyenv = Envir.type_env env;
+    fun etif (Type ("fun", [T, U]), t) =
+          Abs ("", T, etif (U, incr_boundvars 1 t $ Bound 0))
+      | etif (TVar v, t) =
+          (case Type.lookup tyenv v of
+            NONE => t
+          | SOME T => etif (T, t))
+      | etif (_, t) = t;
+    fun eta_nm (rbinder, Abs (a, T, body)) =
+          Abs (a, T, eta_nm ((a, T) :: rbinder, body))
+      | eta_nm (rbinder, t) = etif (fastype env (rbinder, t), t);
   in eta_nm end;
 
 
@@ -186,11 +198,14 @@
 exception ASSIGN; (*Raised if not an assignment*)
 
 
-fun unify_types thy (T,U, env as Envir.Envir{asol,iTs,maxidx}) =
-  if T=U then env
-  else let val (iTs',maxidx') = Sign.typ_unify thy (U, T) (iTs, maxidx)
-       in Envir.Envir{asol=asol,maxidx=maxidx',iTs=iTs'} end
-       handle Type.TUNIFY => raise CANTUNIFY;
+fun unify_types thy (T, U, env) =
+  if T = U then env
+  else
+    let
+      val Envir.Envir {maxidx, tenv, tyenv} = env;
+      val (tyenv', maxidx') = Sign.typ_unify thy (U, T) (tyenv, maxidx);
+    in Envir.Envir {maxidx = maxidx', tenv = tenv, tyenv = tyenv'} end
+    handle Type.TUNIFY => raise CANTUNIFY;
 
 fun test_unify_types thy (args as (T,U,_)) =
 let val str_of = Syntax.string_of_typ_global thy;
@@ -636,9 +651,9 @@
 
 
 (*Pattern matching*)
-fun first_order_matchers thy pairs (Envir.Envir {asol = tenv, iTs = tyenv, maxidx}) =
+fun first_order_matchers thy pairs (Envir.Envir {maxidx, tenv, tyenv}) =
   let val (tyenv', tenv') = fold (Pattern.first_order_match thy) pairs (tyenv, tenv)
-  in Seq.single (Envir.Envir {asol = tenv', iTs = tyenv', maxidx = maxidx}) end
+  in Seq.single (Envir.Envir {maxidx = maxidx, tenv = tenv', tyenv = tyenv'}) end
   handle Pattern.MATCH => Seq.empty;
 
 (*General matching -- keeps variables disjoint*)
@@ -661,10 +676,12 @@
           Term.map_aterms (fn t as Var ((x, i), T) =>
             if i > maxidx then Var ((x, i - offset), T) else t | t => t);
 
-        fun norm_tvar (Envir.Envir {iTs = tyenv, ...}) ((x, i), S) =
-          ((x, i - offset), (S, decr_indexesT (Envir.norm_type tyenv (TVar ((x, i), S)))));
-        fun norm_var (env as Envir.Envir {iTs = tyenv, ...}) ((x, i), T) =
+        fun norm_tvar env ((x, i), S) =
+          ((x, i - offset),
+            (S, decr_indexesT (Envir.norm_type (Envir.type_env env) (TVar ((x, i), S)))));
+        fun norm_var env ((x, i), T) =
           let
+            val tyenv = Envir.type_env env;
             val T' = Envir.norm_type tyenv T;
             val t' = Envir.norm_term env (Var ((x, i), T'));
           in ((x, i - offset), (decr_indexesT T', decr_indexes t')) end;
@@ -672,8 +689,8 @@
         fun result env =
           if Envir.above env maxidx then   (* FIXME proper handling of generated vars!? *)
             SOME (Envir.Envir {maxidx = maxidx,
-              iTs = Vartab.make (map (norm_tvar env) pat_tvars),
-              asol = Vartab.make (map (norm_var env) pat_vars)})
+              tyenv = Vartab.make (map (norm_tvar env) pat_tvars),
+              tenv = Vartab.make (map (norm_var env) pat_vars)})
           else NONE;
 
         val empty = Envir.empty maxidx';
diff -r c141f139ce26 -r b3eaeb39da83 src/Tools/Compute_Oracle/linker.ML
--- a/src/Tools/Compute_Oracle/linker.ML	Fri Jul 17 13:12:18 2009 -0400
+++ b/src/Tools/Compute_Oracle/linker.ML	Fri Jul 17 23:13:57 2009 +0200
@@ -341,7 +341,7 @@
 	    let
 		val (newsubsts, instances) = Linker.add_instances thy instances monocs
 		val _ = if not (null newsubsts) then changed := true else ()
-		val newpats = map (fn subst => Envir.subst_TVars subst p) newsubsts
+		val newpats = map (fn subst => Envir.subst_term_types subst p) newsubsts
 	    in
 		PolyPattern (p, instances, instancepats@newpats)
 	    end 
diff -r c141f139ce26 -r b3eaeb39da83 src/Tools/coherent.ML
--- a/src/Tools/coherent.ML	Fri Jul 17 13:12:18 2009 -0400
+++ b/src/Tools/coherent.ML	Fri Jul 17 23:13:57 2009 +0200
@@ -131,7 +131,7 @@
   let val seq = Seq.of_list rules |> Seq.maps (fn (th, ps, cs) =>
     valid_conj ctxt facts empty_env ps |> Seq.maps (fn (env as (tye, _), is) =>
       let val cs' = map (fn (Ts, ts) =>
-        (map (Envir.typ_subst_TVars tye) Ts, map (Envir.subst_vars env) ts)) cs
+        (map (Envir.subst_type tye) Ts, map (Envir.subst_term env) ts)) cs
       in
         inst_extra_vars ctxt dom cs' |>
           Seq.map_filter (fn (inst, cs'') =>
@@ -184,7 +184,7 @@
             (Thm.ctyp_of thy (TVar ((ixn, S))), Thm.ctyp_of thy T))
                (Vartab.dest tye),
           map (fn (ixn, (T, t)) =>
-            (Thm.cterm_of thy (Var (ixn, Envir.typ_subst_TVars tye T)),
+            (Thm.cterm_of thy (Var (ixn, Envir.subst_type tye T)),
              Thm.cterm_of thy t)) (Vartab.dest env) @
           map (fn (ixnT, t) =>
             (Thm.cterm_of thy (Var ixnT), Thm.cterm_of thy t)) insts) th)
diff -r c141f139ce26 -r b3eaeb39da83 src/Tools/eqsubst.ML
--- a/src/Tools/eqsubst.ML	Fri Jul 17 13:12:18 2009 -0400
+++ b/src/Tools/eqsubst.ML	Fri Jul 17 23:13:57 2009 +0200
@@ -231,9 +231,9 @@
          or should I be using them somehow? *)
           fun mk_insts env =
             (Vartab.dest (Envir.type_env env),
-             Envir.alist_of env);
-          val initenv = Envir.Envir {asol = Vartab.empty,
-                                     iTs = typinsttab, maxidx = ix2};
+             Vartab.dest (Envir.term_env env));
+          val initenv =
+            Envir.Envir {maxidx = ix2, tenv = Vartab.empty, tyenv = typinsttab};
           val useq = Unify.smash_unifiers thry [a] initenv
 	            handle UnequalLengths => Seq.empty
 		               | Term.TERM _ => Seq.empty;
diff -r c141f139ce26 -r b3eaeb39da83 src/Tools/induct.ML
--- a/src/Tools/induct.ML	Fri Jul 17 13:12:18 2009 -0400
+++ b/src/Tools/induct.ML	Fri Jul 17 23:13:57 2009 +0200
@@ -423,14 +423,15 @@
 
 local
 
-fun dest_env thy (env as Envir.Envir {iTs, ...}) =
+fun dest_env thy env =
   let
     val cert = Thm.cterm_of thy;
     val certT = Thm.ctyp_of thy;
-    val pairs = Envir.alist_of env;
+    val pairs = Vartab.dest (Envir.term_env env);
+    val types = Vartab.dest (Envir.type_env env);
     val ts = map (cert o Envir.norm_term env o #2 o #2) pairs;
     val xs = map2 (curry (cert o Var)) (map #1 pairs) (map (#T o Thm.rep_cterm) ts);
-  in (map (fn (xi, (S, T)) => (certT (TVar (xi, S)), certT T)) (Vartab.dest iTs), xs ~~ ts) end;
+  in (map (fn (xi, (S, T)) => (certT (TVar (xi, S)), certT T)) types, xs ~~ ts) end;
 
 in
 
@@ -450,8 +451,7 @@
         val rule' = Thm.incr_indexes (maxidx + 1) rule;
         val concl = Logic.strip_assums_concl goal;
       in
-        Unify.smash_unifiers thy [(Thm.concl_of rule', concl)]
-          (Envir.empty (#maxidx (Thm.rep_thm rule')))
+        Unify.smash_unifiers thy [(Thm.concl_of rule', concl)] (Envir.empty (Thm.maxidx_of rule'))
         |> Seq.map (fn env => Drule.instantiate (dest_env thy env) rule')
       end
   end handle Subscript => Seq.empty;