| changeset 39302 | d7728f65b353 |
| parent 39268 | a56f931fffff |
| child 39355 | 104a6d9e493e |
--- a/src/HOL/Tools/Sledgehammer/clausifier.ML Mon Sep 13 08:43:48 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/clausifier.ML Mon Sep 13 11:13:15 2010 +0200 @@ -78,7 +78,7 @@ (**** REPLACING ABSTRACTIONS BY COMBINATORS ****) -val fun_cong_all = @{thm ext_iff [THEN iffD1]} +val fun_cong_all = @{thm fun_eq_iff [THEN iffD1]} (* Removes the lambdas from an equation of the form "t = (%x. u)". (Cf. "extensionalize_term" in "Sledgehammer_Translate".) *)