# HG changeset patch
# User wenzelm
# Date 1133560487 -3600
# Node ID ed2d0e60fbcc9b3ca0c67a0c8790a1da64c46ac7
# Parent  5d24dbd5e93d80cd228cc229c00b8c9545daea54
defs: beta/eta contract lhs;

diff -r 5d24dbd5e93d -r ed2d0e60fbcc src/Pure/theory.ML
--- a/src/Pure/theory.ML	Fri Dec 02 22:54:45 2005 +0100
+++ b/src/Pure/theory.ML	Fri Dec 02 22:54:47 2005 +0100
@@ -260,7 +260,7 @@
 
     val (lhs, rhs) = Logic.dest_equals (Logic.strip_imp_concl tm)
       handle TERM _ => err "Not a meta-equality (==)";
-    val (head, args) = Term.strip_comb lhs;
+    val (head, args) = Term.strip_comb (Pattern.beta_eta_contract lhs);
     val (c, T) = Term.dest_Const head
       handle TERM _ => err "Head of lhs not a constant";