src/Pure/pattern.ML

   | ints_of (Bound i ::bs) = 
       let val is = ints_of bs
       in if i mem_int is then raise Pattern else i::is end
   | ints_of _              = raise Pattern;
 
+fun ints_of' env ts = ints_of (map (Envir.head_norm env) ts);
+
 
 fun app (s,(i::is)) = app (s$Bound(i),is)
   | app (s,[])      = s;
 
 fun red (Abs(_,_,s)) (i::is) js = red s is (i::js)

 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(T,length is,js))
   in Envir.update((F,mkhnf(binders,is,G,js)),env') end;
-
-
-fun devar env t = case strip_comb t of
-        (Var(F,_),ys) =>
-            (case Envir.lookup(env,F) of
-               Some(t) => devar env (red t (ints_of  ys) []) 
-             | None    => t)
-      |  _            => t;
 
 
 (* 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 i >= 0 then j :: mk(is,j-1) else mk(is,j-1)
           | mk([],_)    = []
     in mk(is,length is - 1) end;
 
 fun proj(s,env,binders,is) =
     let fun trans d i = if i<d then i else (idx is (i-d))+d;
-        fun pr(s,env,d,binders) = (case devar env s of
+        fun pr(s,env,d,binders) = (case Envir.head_norm env s of
               Abs(a,T,t) => let val (t',env') = pr(t,env,d+1,((a,T)::binders))
                             in (Abs(a,T,t'),env') end
             | t => (case strip_comb t of
                 (c as Const _,ts) =>
                          let val (ts',env') = prs(ts,env,d,binders)

                          in if j < 0 then raise Unif
                             else let val (ts',env') = prs(ts,env,d,binders)
                                  in (list_comb(Bound j,ts'),env') end
                          end
                  | (Var(F as (a,_),Fty),ts) =>
-                      let val js = ints_of ts;
+                      let val js = ints_of' env ts;
                           val js' = map (trans d) js;
                           val ks = mk_proj_list js';
                           val ls = filter (fn i => i >= 0) js'
                           val Hty = type_of_G(Fty,length js,ks)
                           val (env',H) = Envir.genvar a (env,Hty)

   if T=U then env
   else let val (iTs',maxidx') = Type.unify (!tsgr) maxidx iTs (U,T)
        in Envir.Envir{asol=asol,maxidx=maxidx',iTs=iTs'} end
        handle Type.TUNIFY => raise Unif;
 
-fun unif binders (env,(s,t)) = case (devar env s,devar env t) of
+fun unif binders (env,(s,t)) = case (Envir.head_norm env s, Envir.head_norm env t) of
       (Abs(ns,Ts,ts),Abs(nt,Tt,tt)) =>
          let val name = if ns = "" then nt else ns
          in unif ((name,Ts)::binders) (env,(ts,tt)) end
     | (Abs(ns,Ts,ts),t) => unif ((ns,Ts)::binders) (env,(ts,(incr t)$Bound(0)))
     | (t,Abs(nt,Tt,tt)) => unif ((nt,Tt)::binders) (env,((incr t)$Bound(0),tt))
     | p => cases(binders,env,p)
 
 and cases(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 ss,ints_of ts)
-                  else flexflex2(env,binders,F,Fty,ints_of ss,G,Gty,ints_of ts)
-      | ((Var(F,_),ss),_)             => flexrigid(env,binders,F,ints_of ss,t)
-      | (_,(Var(F,_),ts))             => flexrigid(env,binders,F,ints_of ts,s)
+         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(env,binders,F,ints_of' env ss,t)
+      | (_,(Var(F,_),ts))             => flexrigid(env,binders,F,ints_of' env ts,s)
       | ((Const c,ss),(Const d,ts))   => rigidrigid(env,binders,c,d,ss,ts)
       | ((Free(f),ss),(Free(g),ts))   => rigidrigid(env,binders,f,g,ss,ts)
       | ((Bound(i),ss),(Bound(j),ts)) => rigidrigidB (env,binders,i,j,ss,ts) 
       | ((Abs(_),_),_)                => raise Pattern
       | (_,(Abs(_),_))                => raise Pattern

 	  if loose_bvar1(f,0) then Abs(a,T,body')
 	  else incr_boundvars ~1 f 
       | body' => Abs(a,T,body'))
   | eta_contract(f$t) = eta_contract f $ eta_contract t
   | eta_contract t = t;
-
-
-(* sharing:
-local
-
-fun eta(Abs(x,T,t)) =
-     (case eta t of
-        None => (case t of
-                   f $ Bound 0 => if loose_bvar1(f,0)
-                                  then None
-                                  else Some(incr_boundvars ~1 f)
-                 | _ => None)
-      | Some(t') => (case t' of
-                       f $ Bound 0 => if loose_bvar1(f,0)
-                                      then Some(Abs(x,T,t'))
-                                      else Some(incr_boundvars ~1 f)
-                     | _ => Some(Abs(x,T,t'))))
-  | eta(s$t) = (case (eta s,eta t) of
-                  (None,   None)    => None
-                | (None,   Some t') => Some(s  $ t')
-                | (Some s',None)    => Some(s' $ t)
-                | (Some s',Some t') => Some(s' $ t'))
-  | eta _ = None
-
-in
-
-fun eta_contract t = case eta t of None => t | Some(t') => t';
-
-end; *)
 
 (*Eta-contract a term from outside: just enough to reduce it to an atom
 DOESN'T QUITE WORK!
 *)
 fun eta_contract_atom (t0 as Abs(a, T, body)) =