preventing eta-redexes in theorems from causing failure
authorpaulson
Fri Oct 12 15:46:29 2007 +0200 (2007-10-12)
changeset 2500838f4ecb71e8c
parent 25007 cd497f6fe8d1
child 25009 61946780de00
preventing eta-redexes in theorems from causing failure
src/HOL/Tools/res_hol_clause.ML
     1.1 --- a/src/HOL/Tools/res_hol_clause.ML	Fri Oct 12 15:45:42 2007 +0200
     1.2 +++ b/src/HOL/Tools/res_hol_clause.ML	Fri Oct 12 15:46:29 2007 +0200
     1.3 @@ -152,7 +152,7 @@
     1.4    | combterm_of thy (t as Abs _) = raise RC.CLAUSE("HOL CLAUSE",t);
     1.5  
     1.6  fun predicate_of thy ((Const("Not",_) $ P), polarity) = predicate_of thy (P, not polarity)
     1.7 -  | predicate_of thy (t,polarity) = (combterm_of thy t, polarity);
     1.8 +  | predicate_of thy (t,polarity) = (combterm_of thy (Envir.eta_contract t), polarity);
     1.9  
    1.10  fun literals_of_term1 thy args (Const("Trueprop",_) $ P) = literals_of_term1 thy args P
    1.11    | literals_of_term1 thy args (Const("op |",_) $ P $ Q) =