src/Pure/pattern.ML

--- a/src/Pure/pattern.ML	Thu Apr 29 15:35:40 1999 +0200
+++ b/src/Pure/pattern.ML	Thu Apr 29 18:33:31 1999 +0200
@@ -271,7 +271,9 @@
 
 end; *)
 
-(*Eta-contract a term from outside: just enough to reduce it to an atom*)
+(*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)) = 
       (case  eta_contract2 body  of
         body' as (f $ Bound 0) =>