src/Pure/pattern.ML

                   "\nCannot unify!\n")
        end
   else ()
 
 fun occurs(F,t,env) =
-    let fun occ(Var (G, T))   = (case Envir.lookup (env, (G, T)) 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, T), mkhnf (binders, is, G, js)), env') end;
+  in Envir.update ((F, T), mkhnf (binders, is, G, js)) env' end;
 
 
 (*predicate: downto0 (is, n) <=> is = [n, n - 1, ..., 0]*)
 fun downto0 (i :: is, n) = i = n andalso downto0 (is, n - 1)
   | downto0 ([], n) = n = ~1;

                           val ks = mk_proj_list js';
                           val ls = map_filter 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, Fty), 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 subset (op =) (js, is)
             then let val t= mkabs(binders,is,app(Var(G,Gty),map (idx is) js))
-                 in Envir.update (((F, Fty), t), env) end
+                 in Envir.update ((F, Fty), t) env end
             else let val ks = inter (op =) js is
                      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, Gty), lam js), Envir.update (((F, Fty), lam is), env'))
+                 in Envir.update ((G, Gty), lam js) (Envir.update ((F, Fty), lam is) env')
                  end;
   in if Term_Ord.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 {maxidx, tenv, tyenv}) =
   if T = U then env

      else fold (unif thy binders) (ss~~ts) env
 
 and flexrigid thy (params as (env,binders,F,Fty,is,t)) =
       if occurs(F,t,env) then (ocheck_fail thy (F,t,binders,env); raise Unif)
       else (let val (u,env') = proj(t,env,binders,is)
-            in Envir.update (((F, Fty), mkabs (binders, is, u)), env') end
+            in Envir.update ((F, Fty), mkabs (binders, is, u)) env' end
             handle Unif => (proj_fail thy params; raise Unif));
 
 fun unify thy = unif thy [];
 
 

 fun first_order_match thy =
   let
     fun mtch k (instsp as (tyinsts,insts)) = fn
         (Var(ixn,T), t)  =>
           if k > 0 andalso Term.is_open t then raise MATCH
-          else (case Envir.lookup' (insts, (ixn, T)) of
+          else (case Envir.lookup1 insts (ixn, T) of
                   NONE => (typ_match thy (T, fastype_of t) tyinsts,
                            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 thy (T,U) tyinsts, insts) else raise MATCH

               if a <> b then raise MATCH
               else rigrig1(typ_match thy (Ta,Tb) iTs, oargs)
     in case ph of
          Var(ixn,T) =>
            let val is = ints_of pargs
-           in case Envir.lookup' (itms, (ixn, T)) of
+           in case Envir.lookup1 itms (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
        | _ =>