# HG changeset patch
# User berghofe
# Date 1114103523 -7200
# Node ID a6360558257318e8beb7c055f1d59ff24cc72a2c
# Parent  348ce23d2fc2d2c5a2918fd3d3f4bb92d5782968
- Eliminated nodup_vars check.
- Unification and matching functions now check types of term variables / sorts
  of type variables when applying a substitution.
- Thm.instantiate now takes (ctyp * ctyp) list instead of (indexname * ctyp) list
  as argument, to allow for proper instantiation of theorems containing
  type variables with same name but different sorts.

diff -r 348ce23d2fc2 -r a63605582573 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Thu Apr 21 19:02:54 2005 +0200
+++ b/src/Pure/drule.ML	Thu Apr 21 19:12:03 2005 +0200
@@ -17,11 +17,13 @@
   val strip_imp_prems   : cterm -> cterm list
   val strip_imp_concl   : cterm -> cterm
   val cprems_of         : thm -> cterm list
+  val cterm_fun         : (term -> term) -> (cterm -> cterm)
+  val ctyp_fun          : (typ -> typ) -> (ctyp -> ctyp)
   val read_insts        :
           Sign.sg -> (indexname -> typ option) * (indexname -> sort option)
                   -> (indexname -> typ option) * (indexname -> sort option)
                   -> string list -> (indexname * string) list
-                  -> (indexname*ctyp)list * (cterm*cterm)list
+                  -> (ctyp * ctyp) list * (cterm * cterm) list
   val types_sorts: thm -> (indexname-> typ option) * (indexname-> sort option)
   val strip_shyps_warning : thm -> thm
   val forall_intr_list  : cterm list -> thm -> thm
@@ -36,7 +38,7 @@
   val implies_elim_list : thm -> thm list -> thm
   val implies_intr_list : cterm list -> thm -> thm
   val instantiate       :
-    (indexname * ctyp) list * (cterm * cterm) list -> thm -> thm
+    (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm
   val zero_var_indexes  : thm -> thm
   val standard          : thm -> thm
   val standard'         : thm -> thm
@@ -131,7 +133,7 @@
   val rename_bvars': string option list -> thm -> thm
   val unvarifyT: thm -> thm
   val unvarify: thm -> thm
-  val tvars_intr_list: string list -> thm -> thm * (string * indexname) list
+  val tvars_intr_list: string list -> thm -> thm * (string * (indexname * sort)) list
   val remdups_rl: thm
   val conj_intr: thm -> thm -> thm
   val conj_intr_list: thm list -> thm
@@ -140,6 +142,8 @@
   val conj_elim_precise: int -> thm -> thm list
   val conj_intr_thm: thm
   val abs_def: thm -> thm
+  val read_instantiate_sg': Sign.sg -> (indexname * string) list -> thm -> thm
+  val read_instantiate': (indexname * string) list -> thm -> thm
 end;
 
 structure Drule: DRULE =
@@ -181,6 +185,14 @@
 (*The premises of a theorem, as a cterm list*)
 val cprems_of = strip_imp_prems o cprop_of;
 
+fun cterm_fun f ct =
+  let val {t, sign, ...} = Thm.rep_cterm ct
+  in Thm.cterm_of sign (f t) end;
+
+fun ctyp_fun f cT =
+  let val {T, sign, ...} = Thm.rep_ctyp cT
+  in Thm.ctyp_of sign (f T) end;
+
 val proto_sign = Theory.sign_of ProtoPure.thy;
 
 val implies = cterm_of proto_sign Term.implies;
@@ -223,8 +235,9 @@
     fun is_tv ((a, _), _) =
       (case Symbol.explode a of "'" :: _ => true | _ => false);
     val (tvs, vs) = List.partition is_tv insts;
+    fun sort_of ixn = case rsorts ixn of SOME S => S | NONE => absent ixn;
     fun readT (ixn, st) =
-        let val S = case rsorts ixn of SOME S => S | NONE => absent ixn;
+        let val S = sort_of ixn;
             val T = Sign.read_typ (sign,sorts) st;
         in if Sign.typ_instance sign (T, TVar(ixn,S)) then (ixn,T)
            else inst_failure ixn
@@ -241,7 +254,8 @@
         let val U = typ_subst_TVars tye2 T
         in cterm_of sign (Var(ixn,U)) end
     val ixnTs = ListPair.zip(ixns, map snd sTs)
-in (map (fn (ixn,T) => (ixn,ctyp_of sign T)) (tye2 @ tye),
+in (map (fn (ixn, T) => (ctyp_of sign (TVar (ixn, sort_of ixn)),
+      ctyp_of sign T)) (tye2 @ tye),
     ListPair.zip(map mkcVar ixnTs,cts))
 end;
 
@@ -380,12 +394,12 @@
             foldr add_term_tvars 
                   (foldr add_term_tvars (term_tvars prop) tpair_l) tpair_r;
         val nms' = rev(Library.foldl add_new_id ([], map (#1 o #1) inrs));
-        val tye = ListPair.map (fn ((v,rs),a) => (v, TVar((a,0),rs)))
+        val tye = ListPair.map (fn ((v, rs), a) => (TVar (v, rs), TVar ((a, 0), rs)))
                      (inrs, nms')
-        val ctye = map (fn (v,T) => (v,ctyp_of sign T)) tye;
+        val ctye = map (pairself (ctyp_of sign)) tye;
         fun varpairs([],[]) = []
           | varpairs((var as Var(v,T)) :: vars, b::bs) =
-                let val T' = typ_subst_TVars tye T
+                let val T' = typ_subst_atomic tye T
                 in (cterm_of sign (Var(v,T')),
                     cterm_of sign (Var((b,0),T'))) :: varpairs(vars,bs)
                 end
@@ -820,16 +834,21 @@
 (*Version that normalizes the result: Thm.instantiate no longer does that*)
 fun instantiate instpair th = Thm.instantiate instpair th  COMP   asm_rl;
 
-fun read_instantiate_sg sg sinsts th =
+fun read_instantiate_sg' sg sinsts th =
     let val ts = types_sorts th;
         val used = add_used th [];
-        val sinsts' = map (apfst Syntax.indexname) sinsts
-    in  instantiate (read_insts sg ts ts used sinsts') th  end;
+    in  instantiate (read_insts sg ts ts used sinsts) th  end;
+
+fun read_instantiate_sg sg sinsts th =
+  read_instantiate_sg' sg (map (apfst Syntax.indexname) sinsts) th;
 
 (*Instantiate theorem th, reading instantiations under theory of th*)
 fun read_instantiate sinsts th =
     read_instantiate_sg (Thm.sign_of_thm th) sinsts th;
 
+fun read_instantiate' sinsts th =
+    read_instantiate_sg' (Thm.sign_of_thm th) sinsts th;
+
 
 (*Left-to-right replacements: tpairs = [...,(vi,ti),...].
   Instantiates distinct Vars by terms, inferring type instantiations. *)
@@ -846,9 +865,9 @@
 fun cterm_instantiate ctpairs0 th =
   let val (sign,tye,_) = foldr add_types (Thm.sign_of_thm th, Vartab.empty, 0) ctpairs0
       fun instT(ct,cu) = 
-        let val inst = cterm_of sign o subst_TVars_Vartab tye o term_of
+        let val inst = cterm_of sign o Envir.subst_TVars tye o term_of
         in (inst ct, inst cu) end
-      fun ctyp2 (ix,T) = (ix, ctyp_of sign T)
+      fun ctyp2 (ixn, (S, T)) = (ctyp_of sign (TVar (ixn, S)), ctyp_of sign T)
   in  instantiate (map ctyp2 (Vartab.dest tye), map instT ctpairs0) th  end
   handle TERM _ =>
            raise THM("cterm_instantiate: incompatible signatures",0,[th])
@@ -925,6 +944,10 @@
       (Thm.cterm_of (#sign (Thm.rep_cterm ct)) (Var v), ct)
         handle TYPE (msg, _, _) => err msg;
 
+    fun tyinst_of (v, cT) =
+      (Thm.ctyp_of (#sign (Thm.rep_ctyp cT)) (TVar v), cT)
+        handle TYPE (msg, _, _) => err msg;
+
     fun zip_vars _ [] = []
       | zip_vars (_ :: vs) (NONE :: opt_ts) = zip_vars vs opt_ts
       | zip_vars (v :: vs) (SOME t :: opt_ts) = (v, t) :: zip_vars vs opt_ts
@@ -933,7 +956,7 @@
     (*instantiate types first!*)
     val thm' =
       if forall is_none cTs then thm
-      else Thm.instantiate (zip_vars (map fst (tvars_of thm)) cTs, []) thm;
+      else Thm.instantiate (map tyinst_of (zip_vars (tvars_of thm) cTs), []) thm;
     in
       if forall is_none cts then thm'
       else Thm.instantiate ([], map inst_of (zip_vars (vars_of thm') cts)) thm'
@@ -1000,10 +1023,11 @@
 
 fun tfrees_of thm =
   let val {hyps, prop, ...} = Thm.rep_thm thm
-  in foldr Term.add_term_tfree_names [] (prop :: hyps) end;
+  in foldr Term.add_term_tfrees [] (prop :: hyps) end;
 
 fun tvars_intr_list tfrees thm =
-  Thm.varifyT' (tfrees_of thm \\ tfrees) thm;
+  apsnd (map (fn ((s, S), ixn) => (s, (ixn, S)))) (Thm.varifyT'
+    (gen_rems (op = o apfst fst) (tfrees_of thm, tfrees)) thm);
 
 
 (* increment var indexes *)
diff -r 348ce23d2fc2 -r a63605582573 src/Pure/envir.ML
--- a/src/Pure/envir.ML	Thu Apr 21 19:02:54 2005 +0200
+++ b/src/Pure/envir.ML	Thu Apr 21 19:12:03 2005 +0200
@@ -3,33 +3,39 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1988  University of Cambridge
 
-Environments.  They don't take account that typ is part of variable
-name.  Therefore we check elsewhere that two variables with same names
-and different types cannot occur.
+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
-  datatype env = Envir of {asol: term Vartab.table, iTs: typ Vartab.table, maxidx: int}
-  val type_env: env -> typ Vartab.table
+  type tenv
+  datatype env = Envir of {asol: tenv, iTs: Type.tyenv, maxidx: int}
+  val type_env: env -> Type.tyenv
   exception SAME
   val genvars: string -> env * typ list -> env * term list
   val genvar: string -> env * typ -> env * term
-  val lookup: env * indexname -> term option
-  val update: (indexname * term) * env -> env
+  val lookup: env * (indexname * typ) -> term option
+  val lookup': (Type.tyenv * tenv) * (indexname * typ) -> term option
+  val update: ((indexname * typ) * term) * env -> env
   val empty: int -> env
   val is_empty: env -> bool
   val above: int * env -> bool
-  val vupdate: (indexname * term) * env -> env
-  val alist_of: env -> (indexname * term) list
+  val vupdate: ((indexname * typ) * term) * env -> env
+  val alist_of: env -> (indexname * (typ * term)) list
   val norm_term: env -> term -> term
   val norm_term_same: env -> term -> term
-  val norm_type: typ Vartab.table -> typ -> typ
-  val norm_type_same: typ Vartab.table -> typ -> typ
-  val norm_types_same: typ Vartab.table -> typ list -> typ list
+  val norm_type: Type.tyenv -> typ -> typ
+  val norm_type_same: Type.tyenv -> typ -> typ
+  val norm_types_same: Type.tyenv -> typ list -> typ list
   val beta_norm: term -> term
   val head_norm: env -> 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
 end;
 
 structure Envir : ENVIR =
@@ -38,10 +44,12 @@
 (*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: term Vartab.table,   (*table of assignments to Vars*)
-     iTs: typ Vartab.table}     (*table of assignments to TVars*)
+    {maxidx: int,      (*maximum index of vars*)
+     asol: tenv,       (*table of assignments to Vars*)
+     iTs: Type.tyenv}  (*table of assignments to TVars*)
 
 fun type_env (Envir {iTs, ...}) = iTs;
 
@@ -60,10 +68,46 @@
   let val (env',[v]) = genvars name (env,[T])
   in  (env',v)  end;
 
-fun lookup (Envir{asol,...}, xname) : term option = Vartab.lookup (asol, xname);
+(* de-reference TVars. When dealing with environments produced by *)
+(* matching instead of unification, there is no need to chase     *)
+(* assigned TVars. In this case, set b to false.                  *)
+fun devar b iTs (T as TVar vT) = (case Type.lookup (iTs, vT) of
+      NONE => T
+    | SOME T' => if b then devar true iTs T' else T')
+  | devar b iTs T = T;
+
+fun eq_type b iTs (T, T') =
+  (case (devar b iTs T, devar b iTs T') of
+     (Type (s, Ts), Type (s', Ts')) =>
+       s = s' andalso ListPair.all (eq_type b iTs) (Ts, Ts')
+   | (U, U') => U = U');
+
+fun var_clash ixn T T' = raise TYPE ("Variable " ^
+  quote (Syntax.string_of_vname ixn) ^ " has two distinct types",
+  [T', T], []);
 
-fun update ((xname, t), Envir{maxidx, asol, iTs}) =
-  Envir{maxidx=maxidx, asol=Vartab.update_new ((xname,t), asol), iTs=iTs};
+fun gen_lookup f asol (xname, T) =
+  (case Vartab.lookup (asol, xname) of
+     NONE => NONE
+   | SOME (U, t) => if f (T, U) then SOME t
+       else var_clash xname T U);
+
+(* version ignoring type substitutions *)
+fun lookup1 asol = gen_lookup op = asol;
+
+fun gen_lookup2 b (iTs, asol) =
+  if Vartab.is_empty iTs then lookup1 asol
+  else gen_lookup (eq_type b iTs) asol;
+
+fun lookup2 env = gen_lookup2 true env;
+
+fun lookup (Envir {asol, iTs, ...}, p) = lookup2 (iTs, asol) p;
+
+(* version for matching algorithms, does not chase TVars *)
+fun lookup' (env, p) = gen_lookup2 false env p;
+
+fun update (((xname, T), t), Envir {maxidx, asol, iTs}) =
+  Envir{maxidx=maxidx, asol=Vartab.update_new ((xname, (T, t)), asol), iTs=iTs};
 
 (*The empty environment.  New variables will start with the given index+1.*)
 fun empty m = Envir{maxidx=m, asol=Vartab.empty, iTs=Vartab.empty};
@@ -80,15 +124,15 @@
    | (SOME (_, i), SOME (_, i')) => i > lim andalso i' > lim);
 
 (*Update, checking Var-Var assignments: try to suppress higher indexes*)
-fun vupdate((a,t), env) = case t of
-      Var(name',T) =>
-        if a=name' then env     (*cycle!*)
+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 xless(a, name')  then
-           (case lookup(env,name') of  (*if already assigned, chase*)
-                NONE => update((name', Var(a,T)), env)
-              | SOME u => vupdate((a,u), env))
-        else update((a,t), env)
-    | _ => update((a,t), env);
+           (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*)
@@ -103,8 +147,8 @@
 exception SAME;
 
 fun norm_term1 same (asol,t) : term =
-  let fun norm (Var (w,T)) =
-            (case Vartab.lookup (asol, w) of
+  let fun norm (Var wT) =
+            (case lookup1 asol wT of
                 SOME u => (norm u handle SAME => u)
               | NONE   => raise SAME)
         | norm (Abs(a,T,body)) =  Abs(a, T, norm body)
@@ -120,7 +164,7 @@
 
 fun normT iTs (Type (a, Ts)) = Type (a, normTs iTs Ts)
   | normT iTs (TFree _) = raise SAME
-  | normT iTs (TVar(v, _)) = (case Vartab.lookup (iTs, v) of
+  | normT iTs (TVar vS) = (case Type.lookup (iTs, vS) of
           SOME U => normTh iTs U
         | NONE => raise SAME)
 and normTh iTs T = ((normT iTs T) handle SAME => T)
@@ -133,7 +177,7 @@
   let fun norm (Const (a, T)) = Const(a, normT iTs T)
         | norm (Free (a, T)) = Free(a, normT iTs T)
         | norm (Var (w, T)) =
-            (case Vartab.lookup (asol, w) of
+            (case lookup2 (iTs, asol) (w, T) of
                 SOME u => normh u
               | NONE   => Var(w, normT iTs T))
         | norm (Abs (a, T, body)) =
@@ -169,7 +213,7 @@
 
 fun head_norm env t =
   let
-    fun hnorm (Var (v, T)) = (case lookup (env, v) of
+    fun hnorm (Var vT) = (case lookup (env, vT) of
           SOME u => head_norm env u
         | NONE => raise SAME)
       | hnorm (Abs (a, T, body)) =  Abs (a, T, hnorm body)
@@ -189,8 +233,8 @@
     fun fast Ts (f $ u) =
 	(case fast Ts f of
 	   Type ("fun", [_, T]) => T
-	 | TVar(ixn, _) =>
-		(case Vartab.lookup (iTs, ixn) of
+	 | TVar ixnS =>
+		(case Type.lookup (iTs, ixnS) of
 		   SOME (Type ("fun", [_, T])) => T
 		 | _ => raise TERM (funerr, [f $ u]))
 	 | _ => raise TERM (funerr, [f $ u]))
@@ -203,4 +247,37 @@
       | 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;
+
+(*Substitute for type Vars in a term*)
+val subst_TVars = map_term_types o typ_subst_TVars;
+
+(*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) = getOpt (lookup1 itms ixnT, v)
+        | subst (Abs (a, T, t)) = Abs (a, T, subst t)
+        | subst (f $ t) = subst f $ subst t
+        | subst t = t
+  in subst t end;
+
+(*Substitute for type/term Vars in a term *)
+fun subst_vars (env as (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' (env, (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
+  in subst end;
+
 end;
diff -r 348ce23d2fc2 -r a63605582573 src/Pure/pattern.ML
--- a/src/Pure/pattern.ML	Thu Apr 21 19:02:54 2005 +0200
+++ b/src/Pure/pattern.ML	Thu Apr 21 19:12:03 2005 +0200
@@ -22,9 +22,9 @@
   val beta_eta_contract : term -> term
   val eta_contract_atom : term -> term
   val match             : Type.tsig -> term * term
-                          -> (indexname*typ)list * (indexname*term)list
+                          -> Type.tyenv * Envir.tenv
   val first_order_match : Type.tsig -> term * term
-                          -> (indexname*typ)list * (indexname*term)list
+                          -> Type.tyenv * Envir.tenv
   val matches           : Type.tsig -> term * term -> bool
   val matches_subterm   : Type.tsig -> term * term -> bool
   val unify             : Sign.sg * Envir.env * (term * term)list -> Envir.env
@@ -72,7 +72,7 @@
   if !trace_unify_fail then clash (boundVar binders i) s
   else ()
 
-fun proj_fail sg (env,binders,F,is,t) =
+fun proj_fail sg (env,binders,F,_,is,t) =
   if !trace_unify_fail
   then let val f = Syntax.string_of_vname F
            val xs = bnames binders is
@@ -94,7 +94,7 @@
   else ()
 
 fun occurs(F,t,env) =
-    let fun occ(Var(G,_))   = (case Envir.lookup(env,G) of
+    let fun occ(Var (G, T))   = (case Envir.lookup (env, (G, T)) of
                                  SOME(t) => occ t
                                | NONE    => F=G)
           | occ(t1$t2)      = occ t1 orelse occ t2
@@ -153,7 +153,7 @@
 
 fun mknewhnf(env,binders,is,F as (a,_),T,js) =
   let val (env',G) = Envir.genvar a (env,type_of_G env (T,length is,js))
-  in Envir.update((F,mkhnf(binders,is,G,js)),env') end;
+  in Envir.update (((F, T), mkhnf (binders, is, G, js)), env') end;
 
 
 (* mk_proj_list(is) = [ |is| - k | 1 <= k <= |is| and is[k] >= 0 ] *)
@@ -186,7 +186,7 @@
                           val Hty = type_of_G env (Fty,length js,ks)
                           val (env',H) = Envir.genvar a (env,Hty)
                           val env'' =
-                                Envir.update((F,mkhnf(binders,js,H,ks)),env')
+                            Envir.update (((F, Fty), mkhnf (binders, js, H, ks)), env')
                       in (app(H,ls),env'') end
                  | _  => raise Pattern))
         and prs(s::ss,env,d,binders) =
@@ -216,12 +216,12 @@
   let fun ff(F,Fty,is,G as (a,_),Gty,js) =
             if js subset_int is
             then let val t= mkabs(binders,is,app(Var(G,Gty),map (idx is) js))
-                 in Envir.update((F,t),env) end
+                 in Envir.update (((F, Fty), t), env) end
             else let val ks = is inter_int js
                      val Hty = type_of_G env (Fty,length is,map (idx is) ks)
                      val (env',H) = Envir.genvar a (env,Hty)
                      fun lam(is) = mkabs(binders,is,app(H,map (idx is) ks));
-                 in Envir.update((G,lam js), Envir.update((F,lam is),env'))
+                 in Envir.update (((G, Gty), lam js), Envir.update (((F, Fty), lam is), env'))
                  end;
   in if xless(G,F) then ff(F,Fty,is,G,Gty,js) else ff(G,Gty,js,F,Fty,is) end
 
@@ -243,8 +243,8 @@
        ((Var(F,Fty),ss),(Var(G,Gty),ts)) =>
          if F = G then flexflex1(env,binders,F,Fty,ints_of' env ss,ints_of' env ts)
                   else flexflex2(env,binders,F,Fty,ints_of' env ss,G,Gty,ints_of' env ts)
-      | ((Var(F,_),ss),_)             => flexrigid sg (env,binders,F,ints_of' env ss,t)
-      | (_,(Var(F,_),ts))             => flexrigid sg (env,binders,F,ints_of' env ts,s)
+      | ((Var(F,Fty),ss),_)           => flexrigid sg (env,binders,F,Fty,ints_of' env ss,t)
+      | (_,(Var(F,Fty),ts))           => flexrigid sg (env,binders,F,Fty,ints_of' env ts,s)
       | ((Const c,ss),(Const d,ts))   => rigidrigid sg (env,binders,c,d,ss,ts)
       | ((Free(f),ss),(Free(g),ts))   => rigidrigid sg (env,binders,f,g,ss,ts)
       | ((Bound(i),ss),(Bound(j),ts)) => rigidrigidB sg (env,binders,i,j,ss,ts)
@@ -266,10 +266,10 @@
      if i <> j then (clashBB binders i j; raise Unif)
      else Library.foldl (unif sg binders) (env ,ss~~ts)
 
-and flexrigid sg (params as (env,binders,F,is,t)) =
+and flexrigid sg (params as (env,binders,F,Fty,is,t)) =
       if occurs(F,t,env) then (ocheck_fail sg (F,t,binders,env); raise Unif)
       else (let val (u,env') = proj(t,env,binders,is)
-            in Envir.update((F,mkabs(binders,is,u)),env') end
+            in Envir.update (((F, Fty), mkabs (binders, is, u)), env') end
             handle Unif => (proj_fail sg params; raise Unif));
 
 fun unify(sg,env,tus) = Library.foldl (unif sg []) (env,tus);
@@ -358,9 +358,9 @@
     fun mtch (instsp as (tyinsts,insts)) = fn
         (Var(ixn,T), t)  =>
           if loose_bvar(t,0) then raise MATCH
-          else (case assoc_string_int(insts,ixn) of
+          else (case Envir.lookup' (instsp, (ixn, T)) of
                   NONE => (typ_match tsig (tyinsts, (T, fastype_of t)),
-                           (ixn,t)::insts)
+                           Vartab.update_new ((ixn, (T, t)), insts))
                 | SOME u => if t aeconv u then instsp else raise MATCH)
       | (Free (a,T), Free (b,U)) =>
           if a=b then (typ_match tsig (tyinsts,(T,U)), insts) else raise MATCH
@@ -374,18 +374,18 @@
       | _ => raise MATCH
   in mtch end;
 
-fun first_order_match tsig = apfst Vartab.dest o fomatch tsig (Vartab.empty, []);
+fun first_order_match tsig = fomatch tsig (Vartab.empty, Vartab.empty);
 
 (* Matching of higher-order patterns *)
 
-fun match_bind(itms,binders,ixn,is,t) =
+fun match_bind(itms,binders,ixn,T,is,t) =
   let val js = loose_bnos t
   in if null is
-     then if null js then (ixn,t)::itms else raise MATCH
+     then if null js then Vartab.update_new ((ixn, (T, t)), itms) else raise MATCH
      else if js subset_int is
           then let val t' = if downto0(is,length binders - 1) then t
                             else mapbnd (idx is) t
-               in (ixn, mkabs(binders,is,t')) :: itms end
+               in Vartab.update_new ((ixn, (T, mkabs (binders, is, t'))), itms) end
           else raise MATCH
   end;
 
@@ -397,7 +397,7 @@
       Abs(ns,Ts,ts) =>
         (case obj of
            Abs(nt,Tt,tt) => mtch ((nt,Tt)::binders) (env,(ts,tt))
-         | _ => let val Tt = typ_subst_TVars_Vartab iTs Ts
+         | _ => let val Tt = Envir.typ_subst_TVars iTs Ts
                 in mtch((ns,Tt)::binders)(env,(ts,(incr obj)$Bound(0))) end)
     | _ => (case obj of
               Abs(nt,Tt,tt) =>
@@ -412,10 +412,10 @@
               if a<> b then raise MATCH
               else rigrig1(typ_match tsg (iTs,(Ta,Tb)), oargs)
     in case ph of
-         Var(ixn,_) =>
+         Var(ixn,T) =>
            let val is = ints_of pargs
-           in case assoc_string_int(itms,ixn) of
-                NONE => (iTs,match_bind(itms,binders,ixn,is,obj))
+           in case Envir.lookup' (env, (ixn, T)) of
+                NONE => (iTs,match_bind(itms,binders,ixn,T,is,obj))
               | SOME u => if obj aeconv (red u is []) then env
                           else raise MATCH
            end
@@ -435,10 +435,10 @@
   val pT = fastype_of pat
   and oT = fastype_of obj
   val iTs = typ_match tsg (Vartab.empty, (pT,oT))
-  val insts2 = (iTs,[])
+  val insts2 = (iTs, Vartab.empty)
 
-in apfst Vartab.dest (mtch [] (insts2, po)
-   handle Pattern => fomatch tsg insts2 po)
+in mtch [] (insts2, po)
+   handle Pattern => fomatch tsg insts2 po
 end;
 
 (*Predicate: does the pattern match the object?*)
@@ -486,7 +486,7 @@
 
     fun match_rew tm (tm1, tm2) =
       let val rtm = getOpt (Term.rename_abs tm1 tm tm2, tm2)
-      in SOME (subst_vars (match tsig (tm1, tm)) rtm, rtm)
+      in SOME (Envir.subst_vars (match tsig (tm1, tm)) rtm, rtm)
         handle MATCH => NONE
       end;
 
diff -r 348ce23d2fc2 -r a63605582573 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Thu Apr 21 19:02:54 2005 +0200
+++ b/src/Pure/proofterm.ML	Thu Apr 21 19:12:03 2005 +0200
@@ -69,11 +69,11 @@
   (** proof terms for specific inference rules **)
   val implies_intr_proof : term -> proof -> proof
   val forall_intr_proof : term -> string -> proof -> proof
-  val varify_proof : term -> string list -> proof -> proof
+  val varify_proof : term -> (string * sort) list -> proof -> proof
   val freezeT : term -> proof -> proof
   val rotate_proof : term list -> term -> int -> proof -> proof
   val permute_prems_prf : term list -> int -> int -> proof -> proof
-  val instantiate : (indexname * typ) list -> (term * term) list -> proof -> proof
+  val instantiate : (typ * typ) list -> (term * term) list -> proof -> proof
   val lift_proof : term -> int -> term -> proof -> proof
   val assumption_proof : term list -> term -> int -> proof -> proof
   val bicompose_proof : term list -> term list -> term list -> term option ->
@@ -401,7 +401,8 @@
   | remove_types t = t;
 
 fun remove_types_env (Envir.Envir {iTs, asol, maxidx}) =
-  Envir.Envir {iTs = iTs, asol = Vartab.map remove_types asol, maxidx = maxidx};
+  Envir.Envir {iTs = iTs, asol = Vartab.map (apsnd remove_types) asol,
+    maxidx = maxidx};
 
 fun norm_proof' env prf = norm_proof (remove_types_env env) prf;
 
@@ -530,11 +531,11 @@
 
 fun varify_proof t fixed prf =
   let
-    val fs = add_term_tfree_names (t, []) \\ fixed;
+    val fs = add_term_tfrees (t, []) \\ fixed;
     val ixns = add_term_tvar_ixns (t, []);
-    val fmap = fs ~~ variantlist (fs, map #1 ixns)
+    val fmap = fs ~~ variantlist (map fst fs, map #1 ixns)
     fun thaw (f as (a, S)) =
-      (case assoc (fmap, a) of
+      (case assoc (fmap, f) of
         NONE => TFree f
       | SOME b => TVar ((b, 0), S));
   in map_proof_terms (map_term_types (map_type_tfree thaw)) (map_type_tfree thaw) prf
@@ -598,7 +599,7 @@
 
 fun instantiate vTs tpairs prf =
   map_proof_terms (subst_atomic (map (apsnd remove_types) tpairs) o
-    subst_TVars vTs) (typ_subst_TVars vTs) prf;
+    map_term_types (typ_subst_atomic vTs)) (typ_subst_atomic vTs) prf;
 
 
 (***** lifting *****)
@@ -955,7 +956,7 @@
 
 fun prf_subst (pinst, (tyinsts, insts)) =
   let
-    val substT = typ_subst_TVars_Vartab tyinsts;
+    val substT = Envir.typ_subst_TVars tyinsts;
 
     fun subst' lev (t as Var (ixn, _)) = (case assoc (insts, ixn) of
           NONE => t
diff -r 348ce23d2fc2 -r a63605582573 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Thu Apr 21 19:02:54 2005 +0200
+++ b/src/Pure/pure_thy.ML	Thu Apr 21 19:12:03 2005 +0200
@@ -273,7 +273,8 @@
       fun substsize prop =
             let val pat = extract_term prop
                 val (_,subst) = Pattern.match tsig (pat,obj)
-            in Library.foldl op+ (0, map (size_of_term o snd) subst) end
+            in Vartab.foldl (op + o apsnd (size_of_term o snd o snd)) (0, subst)
+            end
 
       fun thm_ord ((p0,s0,_),(p1,s1,_)) =
             prod_ord (int_ord o pairself (fn 0 => 0 | x => 1)) int_ord ((p0,s0),(p1,s1));
diff -r 348ce23d2fc2 -r a63605582573 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Thu Apr 21 19:02:54 2005 +0200
+++ b/src/Pure/sign.ML	Thu Apr 21 19:12:03 2005 +0200
@@ -47,7 +47,6 @@
   val classes: sg -> class list
   val defaultS: sg -> sort
   val subsort: sg -> sort * sort -> bool
-  val nodup_vars: term -> term
   val of_sort: sg -> typ * sort -> bool
   val witness_sorts: sg -> sort list -> sort list -> (typ * sort) list
   val universal_witness: sg -> (typ * sort) option
@@ -103,8 +102,6 @@
   val read_typ_raw': Syntax.syntax -> sg * (indexname -> sort option) -> string -> typ
   val read_tyname: sg -> string -> typ
   val read_const: sg -> string -> term
-  val inst_typ_tvars: sg -> (indexname * typ) list -> typ -> typ
-  val inst_term_tvars: sg -> (indexname * typ) list -> term -> term
   val infer_types: Pretty.pp -> sg -> (indexname -> typ option) ->
     (indexname -> sort option) -> string list -> bool
     -> xterm list * typ -> term * (indexname * typ) list
@@ -740,53 +737,8 @@
 
   in typ_of ([], tm) end;
 
-(*check for duplicate occurrences of TFree/TVar with distinct sorts*)
-fun nodup_tvars (env, Type (_, Ts)) = nodup_tvars_list (env, Ts)
-  | nodup_tvars (env as (tfrees, tvars), T as TFree (v as (a, S))) =
-      (case assoc_string (tfrees, a) of
-        SOME S' =>
-          if S = S' then env
-          else raise TYPE ("Type variable " ^ quote a ^
-            " has two distinct sorts", [TFree (a, S'), T], [])
-      | NONE => (v :: tfrees, tvars))
-  | nodup_tvars (env as (tfrees, tvars), T as TVar (v as (a, S))) =
-      (case assoc_string_int (tvars, a) of
-        SOME S' =>
-          if S = S' then env
-          else raise TYPE ("Type variable " ^ quote (Syntax.string_of_vname a) ^
-            " has two distinct sorts", [TVar (a, S'), T], [])
-      | NONE => (tfrees, v :: tvars))
-(*equivalent to foldl nodup_tvars_list, but 3X faster under Poly/ML*)
-and nodup_tvars_list (env, []) = env
-  | nodup_tvars_list (env, T :: Ts) = nodup_tvars_list (nodup_tvars (env, T), Ts);
-
 in
 
-(*check for duplicate occurrences of Free/Var with distinct types*)
-fun nodup_vars tm =
-  let
-    fun nodups (envs as (env as (frees, vars), envT)) tm =
-      (case tm of
-        Const (c, T) => (env, nodup_tvars (envT, T))
-      | Free (v as (a, T)) =>
-          (case assoc_string (frees, a) of
-            SOME T' =>
-              if T = T' then (env, nodup_tvars (envT, T))
-              else raise TYPE ("Variable " ^ quote a ^
-                " has two distinct types", [T', T], [])
-          | NONE => ((v :: frees, vars), nodup_tvars (envT, T)))
-      | Var (v as (ixn, T)) =>
-          (case assoc_string_int (vars, ixn) of
-            SOME T' =>
-              if T = T' then (env, nodup_tvars (envT, T))
-              else raise TYPE ("Variable " ^ quote (Syntax.string_of_vname ixn) ^
-                " has two distinct types", [T', T], [])
-          | NONE => ((frees, v :: vars), nodup_tvars (envT, T)))
-      | Bound _ => envs
-      | Abs (_, T, t) => nodups (env, nodup_tvars (envT, T)) t
-      | s $ t => nodups (nodups envs s) t)
-  in nodups (([], []), ([], [])) tm; tm end;
-
 fun certify_term pp sg tm =
   let
     val _ = check_stale sg;
@@ -811,7 +763,6 @@
       | check_atoms _ = ();
   in
     check_atoms tm';
-    nodup_vars tm';
     (tm', type_check pp sg tm', maxidx_of_term tm')
   end;
 
@@ -835,13 +786,6 @@
 
 
 
-(** instantiation **)
-
-fun inst_typ_tvars sg = Type.inst_typ_tvars (pp sg) (tsig_of sg);
-fun inst_term_tvars sg = Type.inst_term_tvars (pp sg) (tsig_of sg);
-
-
-
 (** infer_types **)         (*exception ERROR*)
 
 (*
diff -r 348ce23d2fc2 -r a63605582573 src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Thu Apr 21 19:02:54 2005 +0200
+++ b/src/Pure/tactic.ML	Thu Apr 21 19:12:03 2005 +0200
@@ -94,7 +94,7 @@
   val subgoals_tac      : string list -> int -> tactic
   val subgoals_of_brl   : bool * thm -> int
   val term_lift_inst_rule       :
-      thm * int * (indexname*typ)list * ((indexname*typ)*term)list  * thm
+      thm * int * ((indexname * sort) * typ) list * ((indexname * typ) * term) list * thm
       -> thm
   val instantiate_tac   : (string * string) list -> tactic
   val thin_tac          : string -> int -> tactic
@@ -117,6 +117,7 @@
   val lift_inst_rule'   : thm * int * (indexname * string) list * thm -> thm
   val eres_inst_tac'    : (indexname * string) list -> thm -> int -> tactic
   val res_inst_tac'     : (indexname * string) list -> thm -> int -> tactic
+  val instantiate_tac'  : (indexname * string) list -> tactic
 end;
 
 structure Tactic: TACTIC =
@@ -246,9 +247,7 @@
                                     Logic.incr_indexes(paramTs,inc) t)
     (*Lifts instantiation pair over params*)
     fun liftpair (cv,ct) = (cterm_fun liftvar cv, cterm_fun liftterm ct)
-    fun lifttvar((a,i),ctyp) =
-        let val {T,sign} = rep_ctyp ctyp
-        in  ((a,i+inc), ctyp_of sign (incr_tvar inc T)) end
+    val lifttvar = pairself (ctyp_fun (incr_tvar inc))
 in Drule.instantiate (map lifttvar Tinsts, map liftpair insts)
                      (lift_rule (st,i) rule)
 end;
@@ -278,7 +277,9 @@
     fun liftvar ((a,j), T) = Var((a, j+inc), paramTs---> incr_tvar inc T)
     (*lift only Var, not term, which must be lifted already*)
     fun liftpair (v,t) = (cterm_of sign (liftvar v), cterm_of sign t)
-    fun liftTpair((a,i),T) = ((a,i+inc), ctyp_of sign (incr_tvar inc T))
+    fun liftTpair (((a, i), S), T) =
+      (ctyp_of sign (TVar ((a, i + inc), S)),
+       ctyp_of sign (incr_tvar inc T))
 in Drule.instantiate (map liftTpair Tinsts, map liftpair insts)
                      (lift_rule (st,i) rule)
 end;
@@ -344,6 +345,8 @@
 (*instantiate variables in the whole state*)
 val instantiate_tac = PRIMITIVE o read_instantiate;
 
+val instantiate_tac' = PRIMITIVE o Drule.read_instantiate';
+
 (*Deletion of an assumption*)
 fun thin_tac s = eres_inst_tac [("V",s)] thin_rl;
 
@@ -647,7 +650,7 @@
     val statement = Logic.list_implies (asms, prop);
     val frees = map Term.dest_Free (Term.term_frees statement);
     val fixed_frees = filter_out (fn (x, _) => x mem_string xs) frees;
-    val fixed_tfrees = foldr Term.add_typ_tfree_names [] (map #2 fixed_frees);
+    val fixed_tfrees = foldr Term.add_typ_tfrees [] (map #2 fixed_frees);
     val params = List.mapPartial (fn x => Option.map (pair x) (assoc_string (frees, x))) xs;
 
     fun err msg = raise ERROR_MESSAGE
diff -r 348ce23d2fc2 -r a63605582573 src/Pure/term.ML
--- a/src/Pure/term.ML	Thu Apr 21 19:02:54 2005 +0200
+++ b/src/Pure/term.ML	Thu Apr 21 19:12:03 2005 +0200
@@ -97,7 +97,6 @@
   val subst_bounds: term list * term -> term
   val subst_bound: term * term -> term
   val subst_TVars: (indexname * typ) list -> term -> term
-  val subst_TVars_Vartab: typ Vartab.table -> term -> term
   val betapply: term * term -> term
   val eq_ix: indexname * indexname -> bool
   val ins_ix: indexname * indexname list -> indexname list
@@ -113,9 +112,9 @@
   val could_unify: term * term -> bool
   val subst_free: (term * term) list -> term -> term
   val subst_atomic: (term * term) list -> term -> term
+  val typ_subst_atomic: (typ * typ) list -> typ -> typ
   val subst_vars: (indexname * typ) list * (indexname * term) list -> term -> term
   val typ_subst_TVars: (indexname * typ) list -> typ -> typ
-  val typ_subst_TVars_Vartab : typ Vartab.table -> typ -> typ
   val subst_Vars: (indexname * term) list -> term -> term
   val incr_tvar: int -> typ -> typ
   val xless: (string * int) * indexname -> bool
@@ -656,6 +655,12 @@
             | subst t = getOpt (assoc(instl,t),t)
       in  subst t  end;
 
+(*Replace the ATOMIC type Ti by Ui;    instl = [(T1,U1), ..., (Tn,Un)].*)
+fun typ_subst_atomic [] T = T
+  | typ_subst_atomic instl (Type (s, Ts)) =
+      Type (s, map (typ_subst_atomic instl) Ts)
+  | typ_subst_atomic instl T = getOpt (assoc (instl, T), T);
+
 (*Substitute for type Vars in a type*)
 fun typ_subst_TVars iTs T = if null iTs then T else
   let fun subst(Type(a,Ts)) = Type(a, map subst Ts)
@@ -1034,17 +1039,6 @@
 structure Typtab = TableFun(type key = typ val ord = typ_ord);
 structure Termtab = TableFun(type key = term val ord = term_ord);
 
-(*Substitute for type Vars in a type, version using Vartab*)
-fun typ_subst_TVars_Vartab 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(ixn, _)) =
-            (case Vartab.lookup (iTs, ixn) of NONE => T | SOME(U) => U)
-  in subst T end;
-
-(*Substitute for type Vars in a term, version using Vartab*)
-val subst_TVars_Vartab = map_term_types o typ_subst_TVars_Vartab;
-
 
 (*** Compression of terms and types by sharing common subtrees.
      Saves 50-75% on storage requirements.  As it is a bit slow,
diff -r 348ce23d2fc2 -r a63605582573 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Thu Apr 21 19:02:54 2005 +0200
+++ b/src/Pure/thm.ML	Thu Apr 21 19:12:03 2005 +0200
@@ -26,7 +26,6 @@
   val cterm_of          : Sign.sg -> term -> cterm
   val ctyp_of_term      : cterm -> ctyp
   val read_cterm        : Sign.sg -> string * typ -> cterm
-  val cterm_fun         : (term -> term) -> (cterm -> cterm)
   val adjust_maxidx     : cterm -> cterm
   val read_def_cterm    :
     Sign.sg * (indexname -> typ option) * (indexname -> sort option) ->
@@ -86,11 +85,11 @@
   val implies_intr_hyps : thm -> thm
   val flexflex_rule     : thm -> thm Seq.seq
   val instantiate       :
-    (indexname * ctyp) list * (cterm * cterm) list -> thm -> thm
+    (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm
   val trivial           : cterm -> thm
   val class_triv        : Sign.sg -> class -> thm
   val varifyT           : thm -> thm
-  val varifyT'          : string list -> thm -> thm * (string * indexname) list
+  val varifyT'          : (string * sort) list -> thm -> thm * ((string * sort) * indexname) list
   val freezeT           : thm -> thm
   val dest_state        : thm * int ->
     (term * term) list * term list * term * term
@@ -129,9 +128,9 @@
   val name_thm		: string * thm -> thm
   val rename_boundvars  : term -> term -> thm -> thm
   val cterm_match       : cterm * cterm ->
-    (indexname * ctyp) list * (cterm * cterm) list
+    (ctyp * ctyp) list * (cterm * cterm) list
   val cterm_first_order_match : cterm * cterm ->
-    (indexname * ctyp) list * (cterm * cterm) list
+    (ctyp * ctyp) list * (cterm * cterm) list
   val cterm_incr_indexes : int -> cterm -> cterm
   val terms_of_tpairs   : (term * term) list -> term list
 end;
@@ -187,8 +186,6 @@
   in  Cterm {sign_ref = Sign.self_ref sign, t = t, T = T, maxidx = maxidx}
   end;
 
-fun cterm_fun f (Cterm {sign_ref, t, ...}) = cterm_of (Sign.deref sign_ref) (f t);
-
 
 exception CTERM of string;
 
@@ -221,8 +218,7 @@
 fun capply (Cterm {t=f, sign_ref=sign_ref1, T=Type("fun",[dty,rty]), maxidx=maxidx1})
            (Cterm {t=x, sign_ref=sign_ref2, T, maxidx=maxidx2}) =
       if T = dty then
-        Cterm{t = if maxidx1 >= 0 andalso maxidx2 >= 0 then Sign.nodup_vars (f $ x)
-            else f $ x,  (*no new Vars: no expensive check!*)
+        Cterm{t = f $ x,
           sign_ref=Sign.merge_refs(sign_ref1,sign_ref2), T=rty,
           maxidx=Int.max(maxidx1, maxidx2)}
       else raise CTERM "capply: types don't agree"
@@ -230,7 +226,7 @@
 
 fun cabs (Cterm {t=t1, sign_ref=sign_ref1, T=T1, maxidx=maxidx1})
          (Cterm {t=t2, sign_ref=sign_ref2, T=T2, maxidx=maxidx2}) =
-      Cterm {t=Sign.nodup_vars (lambda t1 t2), sign_ref=Sign.merge_refs(sign_ref1,sign_ref2),
+      Cterm {t = lambda t1 t2, sign_ref = Sign.merge_refs (sign_ref1,sign_ref2),
              T = T1 --> T2, maxidx=Int.max(maxidx1, maxidx2)}
       handle TERM _ => raise CTERM "cabs: first arg is not a variable";
 
@@ -243,15 +239,18 @@
     val tsig = Sign.tsig_of (Sign.deref sign_ref);
     val (Tinsts, tinsts) = mtch tsig (t1, t2);
     val maxidx = Int.max (maxidx1, maxidx2);
-    val vars = map dest_Var (term_vars t1);
-    fun mk_cTinsts (ixn, T) = (ixn, Ctyp {sign_ref = sign_ref, T = T});
-    fun mk_ctinsts (ixn, t) =
-      let val T = typ_subst_TVars Tinsts (valOf (assoc (vars, ixn)))
+    fun mk_cTinsts (ixn, (S, T)) =
+      (Ctyp {sign_ref = sign_ref, T = TVar (ixn, S)},
+       Ctyp {sign_ref = sign_ref, T = T});
+    fun mk_ctinsts (ixn, (T, t)) =
+      let val T = Envir.typ_subst_TVars Tinsts T
       in
         (Cterm {sign_ref = sign_ref, maxidx = maxidx, T = T, t = Var (ixn, T)},
          Cterm {sign_ref = sign_ref, maxidx = maxidx, T = T, t = t})
       end;
-  in (map mk_cTinsts Tinsts, map mk_ctinsts tinsts) end;
+  in (map mk_cTinsts (Vartab.dest Tinsts),
+    map mk_ctinsts (Vartab.dest tinsts))
+  end;
 
 val cterm_match = gen_cterm_match Pattern.match;
 val cterm_first_order_match = gen_cterm_match Pattern.first_order_match;
@@ -417,11 +416,11 @@
 fun add_terms_sorts ([], Ss) = Ss
   | add_terms_sorts (t::ts, Ss) = add_terms_sorts (ts, add_term_sorts (t,Ss));
 
-fun env_codT (Envir.Envir {iTs, ...}) = map snd (Vartab.dest iTs);
+fun env_codT (Envir.Envir {iTs, ...}) = map (snd o snd) (Vartab.dest iTs);
 
 fun add_env_sorts (Envir.Envir {iTs, asol, ...}, Ss) =
-  Vartab.foldl (add_term_sorts o swap o apsnd snd)
-    (Vartab.foldl (add_typ_sorts o swap o apsnd snd) (Ss, iTs), asol);
+  Vartab.foldl (add_term_sorts o swap o apsnd (snd o snd))
+    (Vartab.foldl (add_typ_sorts o swap o apsnd (snd o snd)) (Ss, iTs), asol);
 
 fun add_insts_sorts ((iTs, is), Ss) =
   add_typs_sorts (map snd iTs, add_terms_sorts (map snd is, Ss));
@@ -546,23 +545,6 @@
 
 (*** Meta rules ***)
 
-(*Check that term does not contain same var with different typing/sorting.
-  If this check must be made, recalculate maxidx in hope of preventing its
-  recurrence.*)
-fun nodup_vars (thm as Thm{sign_ref, der, maxidx, shyps, hyps, tpairs, prop}) s =
-  let
-    val prop' = attach_tpairs tpairs prop;
-    val _ = Sign.nodup_vars prop'
-  in Thm {sign_ref = sign_ref,
-          der = der,
-          maxidx = maxidx_of_term prop',
-          shyps = shyps,
-          hyps = hyps,
-          tpairs = tpairs,
-          prop = prop}
-  end handle TYPE(msg,Ts,ts) => raise TYPE(s^": "^msg,Ts,ts);
-
-
 (** 'primitive' rules **)
 
 (*discharge all assumptions t from ts*)
@@ -669,7 +651,7 @@
         Const("all",Type("fun",[Type("fun",[qary,_]),_])) $ A =>
           if T<>qary then
               raise THM("forall_elim: type mismatch", 0, [th])
-          else let val thm = fix_shyps [th] []
+          else fix_shyps [th] []
                     (Thm{sign_ref= Sign.merge_refs(sign_ref,sign_reft),
                          der = Pt.infer_derivs' (Pt.% o rpair (SOME t)) der,
                          maxidx = Int.max(maxidx, maxt),
@@ -677,10 +659,6 @@
                          hyps = hyps,  
                          tpairs = tpairs,
                          prop = betapply(A,t)})
-               in if maxt >= 0 andalso maxidx >= 0
-                  then nodup_vars thm "forall_elim" 
-                  else thm (*no new Vars: no expensive check!*)
-               end
       | _ => raise THM("forall_elim: not quantified", 0, [th])
   end
   handle TERM _ =>
@@ -731,7 +709,7 @@
   in case (prop1,prop2) of
        ((eq as Const("==", Type (_, [T, _]))) $ t1 $ u, Const("==",_) $ u' $ t2) =>
           if not (u aconv u') then err"middle term"
-          else let val thm =      
+          else
                  Thm{sign_ref= merge_thm_sgs(th1,th2), 
                      der = Pt.infer_derivs (Pt.transitive u T) der1 der2,
                      maxidx = Int.max(max1,max2), 
@@ -739,10 +717,6 @@
                      hyps = union_term(hyps1,hyps2),
                      tpairs = tpairs1 @ tpairs2,
                      prop = eq$t1$t2}
-                 in if max1 >= 0 andalso max2 >= 0
-                    then nodup_vars thm "transitive" 
-                    else thm (*no new Vars: no expensive check!*)
-                 end
      | _ =>  err"premises"
   end;
 
@@ -827,8 +801,8 @@
   in case (prop1,prop2)  of
        (Const ("==", Type ("fun", [fT, _])) $ f $ g,
         Const ("==", Type ("fun", [tT, _])) $ t $ u) =>
-          let val _   = chktypes fT tT
-              val thm = (*no fix_shyps*)
+          (chktypes fT tT;
+                        (*no fix_shyps*)
                         Thm{sign_ref = merge_thm_sgs(th1,th2), 
                             der = Pt.infer_derivs
                               (Pt.combination f g t u fT) der1 der2,
@@ -836,11 +810,7 @@
                             shyps = Sorts.union_sort(shyps1,shyps2),
                             hyps = union_term(hyps1,hyps2),
                             tpairs = tpairs1 @ tpairs2,
-                            prop = Logic.mk_equals(f$t, g$u)}
-          in if max1 >= 0 andalso max2 >= 0
-             then nodup_vars thm "combination" 
-             else thm (*no new Vars: no expensive check!*)  
-          end
+                            prop = Logic.mk_equals(f$t, g$u)})
      | _ =>  raise THM("combination: premises", 0, [th1,th2])
   end;
 
@@ -955,6 +925,8 @@
     Pretty.block [Sign.pretty_term sg t, Pretty.str " ::", Pretty.brk 1, Sign.pretty_typ sg T]
   end;
 
+fun prt_type sg_ref T = Sign.pretty_typ (Sign.deref sg_ref) T;
+
 (*For instantiate: process pair of cterms, merge theories*)
 fun add_ctpair ((ct,cu), (sign_ref,tpairs)) =
   let
@@ -968,9 +940,22 @@
       Pretty.fbrk, prt_typing sign_ref_merged u U]), [T,U], [t,u])
   end;
 
-fun add_ctyp ((v,ctyp), (sign_ref',vTs)) =
-  let val Ctyp {T,sign_ref} = ctyp
-  in (Sign.merge_refs(sign_ref,sign_ref'), (v,T)::vTs) end;
+fun add_ctyp ((Ctyp {T = T as TVar (_, S), sign_ref = sign_refT},
+      Ctyp {T = U, sign_ref = sign_refU}), (sign_ref, vTs)) =
+      let
+        val sign_ref_merged = Sign.merge_refs
+          (sign_ref, Sign.merge_refs (sign_refT, sign_refU));
+        val sign = Sign.deref sign_ref_merged
+      in
+        if Type.of_sort (Sign.tsig_of sign) (U, S) then
+          (sign_ref_merged, (T, U) :: vTs)
+        else raise TYPE ("Type not of sort " ^
+          Sign.string_of_sort sign S, [U], [])
+      end
+  | add_ctyp ((Ctyp {T, sign_ref}, _), _) =
+      raise TYPE (Pretty.string_of (Pretty.block
+        [Pretty.str "instantiate: not a type variable",
+         Pretty.fbrk, prt_type sign_ref T]), [T], []);
 
 in
 
@@ -982,7 +967,7 @@
   let val (newsign_ref,tpairs) = foldr add_ctpair (sign_ref,[]) ctpairs;
       val (newsign_ref,vTs) = foldr add_ctyp (newsign_ref,[]) vcTs;
       fun subst t =
-        subst_atomic tpairs (Sign.inst_term_tvars (Sign.deref newsign_ref) vTs t);
+        subst_atomic tpairs (map_term_types (typ_subst_atomic vTs) t);
       val newprop = subst prop;
       val newdpairs = map (pairself subst) dpairs;
       val newth =
@@ -998,7 +983,7 @@
       then raise THM("instantiate: variables not distinct", 0, [th])
       else if not(null(findrep(map #1 vTs)))
       then raise THM("instantiate: type variables not distinct", 0, [th])
-      else nodup_vars newth "instantiate"
+      else newth
   end
   handle TERM _ => raise THM("instantiate: incompatible signatures", 0, [th])
        | TYPE (msg, _, _) => raise THM (msg, 0, [th]);
@@ -1043,21 +1028,18 @@
 (* Replace all TFrees not fixed or in the hyps by new TVars *)
 fun varifyT' fixed (Thm{sign_ref,der,maxidx,shyps,hyps,tpairs,prop}) =
   let
-    val tfrees = foldr add_term_tfree_names fixed hyps;
+    val tfrees = foldr add_term_tfrees fixed hyps;
     val prop1 = attach_tpairs tpairs prop;
     val (prop2, al) = Type.varify (prop1, tfrees);
     val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2)
-  in let val thm = (*no fix_shyps*)
-    Thm{sign_ref = sign_ref, 
+  in (*no fix_shyps*)
+   (Thm{sign_ref = sign_ref, 
         der = Pt.infer_derivs' (Pt.varify_proof prop tfrees) der,
         maxidx = Int.max(0,maxidx), 
         shyps = shyps, 
         hyps = hyps,
         tpairs = rev (map Logic.dest_equals ts),
-        prop = prop3}
-     in (nodup_vars thm "varifyT", al) end
-(* this nodup_vars check can be removed if thms are guaranteed not to contain
-duplicate TVars with different sorts *)
+        prop = prop3}, al)
   end;
 
 val varifyT = #1 o varifyT' [];
@@ -1324,7 +1306,7 @@
 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' = typ_subst_TVars_Vartab iTs T
+            val T' = Envir.typ_subst_TVars iTs T
             (*Must instantiate types of parameters because they are flattened;
               this could be a NEW parameter*)
         in  all T' $ Abs(a, T', norm_term_skip env n t)  end
diff -r 348ce23d2fc2 -r a63605582573 src/Pure/type.ML
--- a/src/Pure/type.ML	Thu Apr 21 19:02:54 2005 +0200
+++ b/src/Pure/type.ML	Thu Apr 21 19:12:03 2005 +0200
@@ -41,18 +41,18 @@
   val no_tvars: typ -> typ
   val varifyT: typ -> typ
   val unvarifyT: typ -> typ
-  val varify: term * string list -> term * (string * indexname) list
+  val varify: term * (string * sort) list -> term * ((string * sort) * indexname) list
   val freeze_thaw_type : typ -> typ * (typ -> typ)
   val freeze_thaw : term -> term * (term -> term)
 
   (*matching and unification*)
-  val inst_typ_tvars: Pretty.pp -> tsig -> (indexname * typ) list -> typ -> typ
-  val inst_term_tvars: Pretty.pp -> tsig -> (indexname * typ) list -> term -> term
   exception TYPE_MATCH
-  val typ_match: tsig -> typ Vartab.table * (typ * typ) -> typ Vartab.table
+  type tyenv
+  val lookup: tyenv * (indexname * sort) -> typ option
+  val typ_match: tsig -> tyenv * (typ * typ) -> tyenv
   val typ_instance: tsig -> typ * typ -> bool
   exception TUNIFY
-  val unify: tsig -> typ Vartab.table * int -> typ * typ -> typ Vartab.table * int
+  val unify: tsig -> tyenv * int -> typ * typ -> tyenv * int
   val raw_unify: typ * typ -> bool
 
   (*extend and merge type signatures*)
@@ -219,11 +219,11 @@
 
 fun varify (t, fixed) =
   let
-    val fs = add_term_tfree_names (t, []) \\ fixed;
+    val fs = add_term_tfrees (t, []) \\ fixed;
     val ixns = add_term_tvar_ixns (t, []);
-    val fmap = fs ~~ map (rpair 0) (variantlist (fs, map #1 ixns))
+    val fmap = fs ~~ map (rpair 0) (variantlist (map fst fs, map #1 ixns))
     fun thaw (f as (a, S)) =
-      (case assoc (fmap, a) of
+      (case assoc (fmap, f) of
         NONE => TFree f
       | SOME b => TVar (b, S));
   in (map_term_types (map_type_tfree thaw) t, fmap) end;
@@ -273,21 +273,15 @@
 
 (** matching and unification of types **)
 
-(* instantiation *)
+type tyenv = (sort * typ) Vartab.table;
 
-fun inst_typ_tvars pp tsig tye =
-  let
-    fun inst (var as (v, S)) =
-      (case assoc_string_int (tye, v) of
-        SOME U =>
-          if of_sort tsig (U, S) then U
-          else raise TYPE ("Type not of sort " ^ Pretty.string_of_sort pp S, [U], [])
-      | NONE => TVar var);
-  in map_type_tvar inst end;
+fun tvar_clash ixn S S' = raise TYPE ("Type variable " ^
+  quote (Term.string_of_vname ixn) ^ " has two distinct sorts",
+  [TVar (ixn, S), TVar (ixn, S')], []);
 
-fun inst_term_tvars _ _ [] t = t
-  | inst_term_tvars pp tsig tye t = map_term_types (inst_typ_tvars pp tsig tye) t;
-
+fun lookup (tye, (ixn, S)) = case Vartab.lookup (tye, ixn) of
+    NONE => NONE
+  | SOME (S', T) => if S = S' then SOME T else tvar_clash ixn S S';
 
 (* matching *)
 
@@ -296,9 +290,9 @@
 fun typ_match tsig =
   let
     fun match (subs, (TVar (v, S), T)) =
-          (case Vartab.lookup (subs, v) of
+          (case lookup (subs, (v, S)) of
             NONE =>
-              if of_sort tsig (T, S) then Vartab.update ((v, T), subs)
+              if of_sort tsig (T, S) then Vartab.update_new ((v, (S, T)), subs)
               else raise TYPE_MATCH
           | SOME U => if U = T then subs else raise TYPE_MATCH)
       | match (subs, (Type (a, Ts), Type (b, Us))) =
@@ -322,16 +316,16 @@
   let
     fun occ (Type (_, Ts)) = exists occ Ts
       | occ (TFree _) = false
-      | occ (TVar (w, _)) =
+      | occ (TVar (w, S)) =
           eq_ix (v, w) orelse
-            (case Vartab.lookup (tye, w) of
+            (case lookup (tye, (w, S)) of
               NONE => false
             | SOME U => occ U);
   in occ end;
 
 (*chase variable assignments; if devar returns a type var then it must be unassigned*)
-fun devar (T as TVar (v, _), tye) =
-      (case  Vartab.lookup (tye, v) of
+fun devar (T as TVar v, tye) =
+      (case  lookup (tye, v) of
         SOME U => devar (U, tye)
       | NONE => T)
   | devar (T, tye) = T;
@@ -347,8 +341,8 @@
     fun meet ((_, []), tye) = tye
       | meet ((TVar (xi, S'), S), tye) =
           if Sorts.sort_le classes (S', S) then tye
-          else Vartab.update_new ((xi,
-            gen_tyvar (Sorts.inter_sort classes (S', S))), tye)
+          else Vartab.update_new ((xi, (S',
+            gen_tyvar (Sorts.inter_sort classes (S', S)))), tye)
       | meet ((TFree (_, S'), S), tye) =
           if Sorts.sort_le classes (S', S) then tye
           else raise TUNIFY
@@ -361,21 +355,22 @@
     fun unif ((ty1, ty2), tye) =
       (case (devar (ty1, tye), devar (ty2, tye)) of
         (T as TVar (v, S1), U as TVar (w, S2)) =>
-          if eq_ix (v, w) then tye
+          if eq_ix (v, w) then
+            if S1 = S2 then tye else tvar_clash v S1 S2
           else if Sorts.sort_le classes (S1, S2) then
-            Vartab.update_new ((w, T), tye)
+            Vartab.update_new ((w, (S2, T)), tye)
           else if Sorts.sort_le classes (S2, S1) then
-            Vartab.update_new ((v, U), tye)
+            Vartab.update_new ((v, (S1, U)), tye)
           else
             let val S = gen_tyvar (Sorts.inter_sort classes (S1, S2)) in
-              Vartab.update_new ((v, S), Vartab.update_new ((w, S), tye))
+              Vartab.update_new ((v, (S1, S)), Vartab.update_new ((w, (S2, S)), tye))
             end
       | (TVar (v, S), T) =>
           if occurs v tye T then raise TUNIFY
-          else meet ((T, S), Vartab.update_new ((v, T), tye))
+          else meet ((T, S), Vartab.update_new ((v, (S, T)), tye))
       | (T, TVar (v, S)) =>
           if occurs v tye T then raise TUNIFY
-          else meet ((T, S), Vartab.update_new ((v, T), tye))
+          else meet ((T, S), Vartab.update_new ((v, (S, T)), tye))
       | (Type (a, Ts), Type (b, Us)) =>
           if a <> b then raise TUNIFY
           else foldr unif tye (Ts ~~ Us)
diff -r 348ce23d2fc2 -r a63605582573 src/Pure/unify.ML
--- a/src/Pure/unify.ML	Thu Apr 21 19:02:54 2005 +0200
+++ b/src/Pure/unify.ML	Thu Apr 21 19:12:03 2005 +0200
@@ -1,13 +1,10 @@
-(*  Title: 	unify
+(*  Title:      Pure/unify.ML
     ID:         $Id$
     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   Cambridge University 1992
 
 Higher-Order Unification
 
-Potential problem: type of Vars is often ignored, so two Vars with same
-indexname but different types can cause errors!
-
 Types as well as terms are unified.  The outermost functions assume the
 terms to be unified already have the same type.  In resolution, this is
 assured because both have type "prop".
@@ -49,14 +46,14 @@
 
 fun body_type(Envir.Envir{iTs,...}) = 
 let fun bT(Type("fun",[_,T])) = bT T
-      | bT(T as TVar(ixn,_)) = (case Vartab.lookup (iTs,ixn) of
+      | bT(T as TVar ixnS) = (case Type.lookup (iTs, ixnS) 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(ixn,_)) = (case Vartab.lookup (iTs,ixn) of
+      | bTs(T as TVar ixnS) = (case Type.lookup (iTs, ixnS) of
 		NONE => [] | SOME(T') => bTs T')
       | bTs _ = []
 in bTs end;
@@ -70,8 +67,8 @@
 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(ixn,_),t) = 
-	    (case Vartab.lookup (iTs,ixn) of
+	| 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)) =
@@ -84,7 +81,11 @@
   Does the uvar occur in the term t?  
   two forms of search, for whether there is a rigid path to the current term.
   "seen" is list of variables passed thru, is a memo variable for sharing.
-  This version searches for nonrigid occurrence, returns true if found. *)
+  This version searches for nonrigid occurrence, returns true if found.
+  Since terms may contain variables with same name and different types,
+  the occurs check must ignore the types of variables. This avoids
+  that ?x::?'a is unified with f(?x::T), which may lead to a cyclic
+  substitution when ?'a is instantiated with T later. *)
 fun occurs_terms (seen: (indexname list) ref,
  		  env: Envir.env, v: indexname, ts: term list): bool =
   let fun occurs [] = false
@@ -92,12 +93,12 @@
       and occur (Const _)  = false
 	| occur (Bound _)  = false
 	| occur (Free _)  = false
-	| occur (Var (w,_))  = 
+	| occur (Var (w, T))  = 
 	    if mem_ix (w, !seen) then false
 	    else if eq_ix(v,w) then true
 	      (*no need to lookup: v has no assignment*)
 	    else (seen := w:: !seen;  
-	          case  Envir.lookup(env,w)  of
+	          case Envir.lookup (env, (w, T)) of
 		      NONE    => false
 		    | SOME t => occur t)
 	| occur (Abs(_,_,body)) = occur body
@@ -109,7 +110,7 @@
 (* f(a1,...,an)  ---->   (f,  [a1,...,an])  using the assignments*)
 fun head_of_in (env,t) : term = case t of
     f$_ => head_of_in(env,f)
-  | Var (v,_) => (case  Envir.lookup(env,v)  of  
+  | Var vT => (case Envir.lookup (env, vT) of  
 			SOME u => head_of_in(env,u)  |  NONE   => t)
   | _ => t;
 
@@ -155,11 +156,11 @@
       and occur (Const _)  = NoOcc
 	| occur (Bound _)  = NoOcc
 	| occur (Free _)  = NoOcc
-	| occur (Var (w,_))  = 
+	| occur (Var (w, T))  = 
 	    if mem_ix (w, !seen) then NoOcc
 	    else if eq_ix(v,w) then Rigid
 	    else (seen := w:: !seen;  
-	          case  Envir.lookup(env,w)  of
+	          case Envir.lookup (env, (w, T)) of
 		      NONE    => NoOcc
 		    | SOME t => occur t)
 	| occur (Abs(_,_,body)) = occur body
@@ -210,11 +211,11 @@
   If v occurs rigidly then nonunifiable.
   If v occurs nonrigidly then must use full algorithm. *)
 fun assignment (env, rbinder, t, u) =
-    let val (v,T) = get_eta_var(rbinder,0,t)
-    in  case rigid_occurs_term (ref[], env, v, u) of
+    let val vT as (v,T) = get_eta_var (rbinder, 0, t)
+    in  case rigid_occurs_term (ref [], env, v, u) of
 	      NoOcc => let val env = unify_types(body_type env T,
 						 fastype env (rbinder,u),env)
-		in Envir.update ((v, rlist_abs(rbinder,u)), env) end
+		in Envir.update ((vT, rlist_abs (rbinder, u)), env) end
 	    | Nonrigid =>  raise ASSIGN
 	    | Rigid =>  raise CANTUNIFY
     end;
@@ -282,7 +283,7 @@
 
 (* changed(env,t) checks whether the head of t is a variable assigned in env*)
 fun changed (env, f$_) = changed (env,f)
-  | changed (env, Var (v,_)) =
+  | changed (env, Var v) =
       (case Envir.lookup(env,v) of NONE=>false  |  _ => true)
   | changed _ = false;
 
@@ -395,12 +396,12 @@
 (*Call matchcopy to produce assignments to the variable in the dpair*)
 fun MATCH (env, (rbinder,t,u), dpairs)
 	: (Envir.env * dpair list)Seq.seq = 
-  let val (Var(v,T), targs) = strip_comb t;
+  let val (Var (vT as (v, T)), targs) = strip_comb t;
       val Ts = binder_types env T;
       fun new_dset (u', (env',dpairs')) =
 	  (*if v was updated to s, must unify s with u' *)
-	  case Envir.lookup(env',v) of
-	      NONE => (Envir.update ((v, types_abs(Ts, u')), env'),  dpairs')
+	  case Envir.lookup (env', vT) of
+	      NONE => (Envir.update ((vT, types_abs(Ts, u')), env'),  dpairs')
 	    | SOME s => (env', ([], s, types_abs(Ts, u'))::dpairs')
   in Seq.map new_dset
          (matchcopy (#1 v) (rbinder, targs, u, (env,dpairs)))
@@ -413,12 +414,12 @@
 (*At end of unification, do flex-flex assignments like ?a -> ?f(?b) 
   Attempts to update t with u, raising ASSIGN if impossible*)
 fun ff_assign(env, rbinder, t, u) : Envir.env = 
-let val (v,T) = get_eta_var(rbinder,0,t)
-in if occurs_terms (ref[], env, v, [u]) then raise ASSIGN
+let val vT as (v,T) = get_eta_var(rbinder,0,t)
+in if occurs_terms (ref [], env, v, [u]) then raise ASSIGN
    else let val env = unify_types(body_type env T,
 				  fastype env (rbinder,u),
 				  env)
-	in Envir.vupdate ((v, rlist_abs(rbinder, u)), env) end
+	in Envir.vupdate ((vT, rlist_abs (rbinder, u)), env) end
 end;
 
 
@@ -494,7 +495,7 @@
     if decreasing (length Ts) args then (env, (list_comb(Var(v,T), ts')))
     else let val (env',v') = Envir.genvar (#1v) (env, map (#T) args ---> U)
 	     val body = list_comb(v', map (Bound o #j) args)
-	     val env2 = Envir.vupdate (((v, types_abs(Ts, body)),   env'))
+	     val env2 = Envir.vupdate ((((v, T), types_abs(Ts, body)),   env'))
 	     (*the vupdate affects ts' if they contain v*)
 	 in  
 	     (env2, Envir.norm_term env2 (list_comb(v',ts')))
@@ -615,12 +616,12 @@
     requires more work yet gives a less general unifier (fewer variables).
   Handles ?f(t1...rm) with ?f(u1...um) to avoid multiple updates. *)
 fun smash_flexflex1 ((t,u), env) : Envir.env =
-  let val (v,T) = var_head_of (env,t)
-      and (w,U) = var_head_of (env,u);
+  let val vT as (v,T) = var_head_of (env,t)
+      and wU as (w,U) = var_head_of (env,u);
       val (env', var) = Envir.genvar (#1v) (env, body_type env T)
-      val env'' = Envir.vupdate((w, type_abs(env',U,var)),  env')
-  in  if (v,T)=(w,U) then env''  (*the other update would be identical*)
-      else Envir.vupdate((v, type_abs(env',T,var)), env'')
+      val env'' = Envir.vupdate ((wU, type_abs (env', U, var)), env')
+  in  if vT = wU then env''  (*the other update would be identical*)
+      else Envir.vupdate ((vT, type_abs (env', T, var)), env'')
   end;