src/Pure/pattern.ML

   val eta_contract      : term -> term
   val eta_long          : typ list -> term -> term
   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
   val first_order       : term -> bool
   val pattern           : term -> bool

 
 fun clashB binders i s =
   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
            val u = string_of_term sg env binders t
            val ys = bnames binders (loose_bnos t \\ is)

                   "\nCannot unify!\n")
        end
   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
           | occ(Abs(_,_,t)) = occ t
           | occ _           = false

 
 fun mkhnf (binders,is,G,js) = mkabs (binders, is, app(G,js));
 
 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 ] *)
 fun mk_proj_list is =
     let fun mk(i::is,j) = if isSome i then j :: mk(is,j-1) else mk(is,j-1)

                           val ks = mk_proj_list js';
                           val ls = List.mapPartial I js'
                           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) =
               let val (s',env1) = pr(s,env,d,binders)
                   val (ss',env2) = prs(ss,env1,d,binders)

 
 fun flexflex2(env,binders,F,Fty,is,G,Gty,js) =
   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
 
 fun unify_types sg (T,U, env as Envir.Envir{asol,iTs,maxidx}) =
   if T=U then env

 
 and cases sg (binders,env,(s,t)) = case (strip_comb s,strip_comb t) of
        ((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)
       | ((Abs(_),_),_)                => raise Pattern
       | (_,(Abs(_),_))                => raise Pattern

 
 and rigidrigidB sg (env,binders,i,j,ss,ts) =
      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);
 
 

 fun fomatch tsig =
   let
     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
       | (Const (a,T), Const (b,U))  =>
           if a=b then (typ_match tsig (tyinsts,(T,U)), insts) else raise MATCH

       | (f$t, g$u) => mtch (mtch instsp (f,g)) (t, u)
       | (t, Abs(_,U,u))  =>  mtch instsp ((incr t)$(Bound 0), u)
       | _ => 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;
 
 fun match tsg (po as (pat,obj)) =
 let

   fun mtch binders (env as (iTs,itms),(pat,obj)) =
     case pat of
       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) =>
                 mtch((nt,Tt)::binders)(env,((incr pat)$Bound(0),tt))
             | _ => cases(binders,env,pat,obj))

               Library.foldl (mtch binders) ((iTs,itms), pargs~~oargs)
         fun rigrig2((a,Ta),(b,Tb),oargs) =
               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
        | _ =>
            let val (oh,oargs) = strip_comb obj

     end;
 
   val pT = fastype_of pat
   and oT = fastype_of obj
   val iTs = typ_match tsg (Vartab.empty, (pT,oT))
-  val insts2 = (iTs,[])
-
-in apfst Vartab.dest (mtch [] (insts2, po)
-   handle Pattern => fomatch tsg insts2 po)
+  val insts2 = (iTs, Vartab.empty)
+
+in mtch [] (insts2, po)
+   handle Pattern => fomatch tsg insts2 po
 end;
 
 (*Predicate: does the pattern match the object?*)
 fun matches tsig po = (match tsig po; true) handle MATCH => false;
 

         val t' = subst_bound (Free (x', T), t);
       in (fn u => Abs (x, T, abstract_over (Free (x', T), u)), t') end;
 
     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;
 
     fun rew (Abs (_, _, body) $ t) = SOME (subst_bound (t, body), skel0)
       | rew tm = (case get_first (match_rew tm) rules of