tuned aeconv: test plain aconv before expensive eta_contract;

--- a/src/Pure/pattern.ML	Mon Mar 16 23:52:30 2009 +0100
+++ b/src/Pure/pattern.ML	Tue Mar 17 12:09:43 2009 +0100
@@ -290,7 +290,8 @@
 
 (*Tests whether 2 terms are alpha/eta-convertible and have same type.
   Note that Consts and Vars may have more than one type.*)
-fun t aeconv u = Envir.eta_contract t aconv Envir.eta_contract u;
+fun t aeconv u = t aconv u orelse
+  Envir.eta_contract t aconv Envir.eta_contract u;
 
 
 (*** Matching ***)