src/Pure/pattern.ML
changeset 30555 5925cd6671d5
parent 29269 5c25a2012975
child 30565 784be11cb70e
     1.1 --- a/src/Pure/pattern.ML	Mon Mar 16 23:52:30 2009 +0100
     1.2 +++ b/src/Pure/pattern.ML	Tue Mar 17 12:09:43 2009 +0100
     1.3 @@ -290,7 +290,8 @@
     1.4  
     1.5  (*Tests whether 2 terms are alpha/eta-convertible and have same type.
     1.6    Note that Consts and Vars may have more than one type.*)
     1.7 -fun t aeconv u = Envir.eta_contract t aconv Envir.eta_contract u;
     1.8 +fun t aeconv u = t aconv u orelse
     1.9 +  Envir.eta_contract t aconv Envir.eta_contract u;
    1.10  
    1.11  
    1.12  (*** Matching ***)