src/Pure/pattern.ML
changeset 6539 2e7d2fba9f6c
parent 4820 8f6dbbd8d497
child 8406 a217b0cd304d
     1.1 --- a/src/Pure/pattern.ML	Thu Apr 29 15:35:40 1999 +0200
     1.2 +++ b/src/Pure/pattern.ML	Thu Apr 29 18:33:31 1999 +0200
     1.3 @@ -271,7 +271,9 @@
     1.4  
     1.5  end; *)
     1.6  
     1.7 -(*Eta-contract a term from outside: just enough to reduce it to an atom*)
     1.8 +(*Eta-contract a term from outside: just enough to reduce it to an atom
     1.9 +DOESN'T QUITE WORK!
    1.10 +*)
    1.11  fun eta_contract_atom (t0 as Abs(a, T, body)) = 
    1.12        (case  eta_contract2 body  of
    1.13          body' as (f $ Bound 0) =>