# HG changeset patch
# User paulson
# Date 1192196789 -7200
# Node ID 38f4ecb71e8c1e358badba778fa4e5a102d7f8a7
# Parent  cd497f6fe8d1a77b7a58efecb576d70104557bf0
preventing eta-redexes in theorems from causing failure

diff -r cd497f6fe8d1 -r 38f4ecb71e8c src/HOL/Tools/res_hol_clause.ML
--- a/src/HOL/Tools/res_hol_clause.ML	Fri Oct 12 15:45:42 2007 +0200
+++ b/src/HOL/Tools/res_hol_clause.ML	Fri Oct 12 15:46:29 2007 +0200
@@ -152,7 +152,7 @@
   | combterm_of thy (t as Abs _) = raise RC.CLAUSE("HOL CLAUSE",t);
 
 fun predicate_of thy ((Const("Not",_) $ P), polarity) = predicate_of thy (P, not polarity)
-  | predicate_of thy (t,polarity) = (combterm_of thy t, polarity);
+  | predicate_of thy (t,polarity) = (combterm_of thy (Envir.eta_contract t), polarity);
 
 fun literals_of_term1 thy args (Const("Trueprop",_) $ P) = literals_of_term1 thy args P
   | literals_of_term1 thy args (Const("op |",_) $ P $ Q) =