# HG changeset patch
# User wenzelm
# Date 1237288183 -3600
# Node ID 5925cd6671d5e8448f68838af5ce7bf06da86ab4
# Parent  73f8bd5f0af818570dd93aa873f72611bf1466f7
tuned aeconv: test plain aconv before expensive eta_contract;

diff -r 73f8bd5f0af8 -r 5925cd6671d5 src/Pure/pattern.ML
--- 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 ***)