# HG changeset patch
# User berghofe
# Date 1006187642 -3600
# Node ID ff75ed08b3fbe8b72f4ea79d1085efbfdcebdd01
# Parent  4a25f04bea6182697035d9e9158b4fa53a6aa755
Replaced devar by Envir.head_norm

diff -r 4a25f04bea61 -r ff75ed08b3fb src/Pure/pattern.ML
--- a/src/Pure/pattern.ML	Mon Nov 19 17:32:49 2001 +0100
+++ b/src/Pure/pattern.ML	Mon Nov 19 17:34:02 2001 +0100
@@ -82,6 +82,8 @@
       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;
@@ -106,14 +108,6 @@
   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)
@@ -122,7 +116,7 @@
 
 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
@@ -139,7 +133,7 @@
                                  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'
@@ -193,7 +187,7 @@
        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
@@ -203,10 +197,10 @@
 
 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) 
@@ -242,35 +236,6 @@
   | 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!
 *)