Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
preventing eta-redexes in theorems from causing failure
authorpaulson
Fri, 12 Oct 2007 15:46:29 +0200
changeset 25008 38f4ecb71e8c
parent 25007 cd497f6fe8d1
child 25009 61946780de00
preventing eta-redexes in theorems from causing failure
src/HOL/Tools/res_hol_clause.ML file | annotate | diff | comparison | revisions 
--- 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) =
isabelle