# HG changeset patch
# User paulson
# Date 857552685 -3600
# Node ID 9453616d4b803e077b4f8eac54907b2f62ebdda3
# Parent  ddc6cf6b62e930c25cad65e7bce146dec7a15748
Declares eta_contract_atom; fixed comment; some tidying

diff -r ddc6cf6b62e9 -r 9453616d4b80 src/Pure/pattern.ML
--- a/src/Pure/pattern.ML	Wed Mar 05 10:03:30 1997 +0100
+++ b/src/Pure/pattern.ML	Wed Mar 05 10:04:45 1997 +0100
@@ -17,11 +17,12 @@
   type type_sig
   type sg
   type env
-  val eta_contract: term -> term
-  val match: type_sig -> term * term
-        -> (indexname*typ)list * (indexname*term)list
-  val matches: type_sig -> term * term -> bool
-  val unify: sg * env * (term * term)list -> env
+  val eta_contract      : term -> term
+  val eta_contract_atom : term -> term
+  val match             : type_sig -> term * term
+                          -> (indexname*typ)list * (indexname*term)list
+  val matches           : type_sig -> term * term -> bool
+  val unify             : sg * env * (term * term)list -> env
   exception Unif
   exception MATCH
   exception Pattern
@@ -221,7 +222,7 @@
                          foldl (unif []) (env,tus));
 
 
-(*Perform eta-contractions upon a term*)
+(*Eta-contract a term (fully)*)
 fun eta_contract (Abs(a,T,body)) = 
       (case  eta_contract body  of
         body' as (f $ Bound 0) => 
@@ -232,6 +233,18 @@
   | eta_contract t = t;
 
 
+(*Eta-contract a term from outside: just enough to reduce it to an atom*)
+fun eta_contract_atom (t0 as Abs(a, T, body)) = 
+      (case  eta_contract2 body  of
+        body' as (f $ Bound 0) => 
+	    if (0 mem_int loose_bnos f) then Abs(a,T,body')
+	    else eta_contract_atom (incr_boundvars ~1 f)
+      | _ => t0)
+  | eta_contract_atom t = t
+and eta_contract2 (f$t) = f $ eta_contract_atom t
+  | eta_contract2 t     = eta_contract_atom t;
+
+
 (* Pattern matching *)
 exception MATCH;
 
@@ -239,8 +252,7 @@
     returns a (tyvar,typ)list and (var,term)list.
   The pattern and object may have variables in common.
   Instantiation does not affect the object, so matching ?a with ?a+1 works.
-  A Const does not match a Free of the same name! 
-  Does not notice eta-equality, thus f does not match %(x)f(x)  *)
+  A Const does not match a Free of the same name! *)
 fun fomatch tsig (pat,obj) =
   let fun typ_match args = (Type.typ_match tsig args)
 			   handle Type.TYPE_MATCH => raise MATCH;
@@ -261,7 +273,7 @@
 	  mtch (typ_match (tyinsts,(T,U)),insts) (t,u)
       | (f$t, g$u) => mtch (mtch (tyinsts,insts) (f,g)) (t, u)
       | _ => raise MATCH
-  in mtch([],[]) (eta_contract pat,eta_contract obj) end;
+  in mtch([],[]) (eta_contract pat, eta_contract obj) end;
 
 
 fun match_bind(itms,binders,ixn,is,t) =