diff -r a2c3706c4cb1 -r aada9fd08b58 src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue May 22 16:59:27 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue May 22 16:59:27 2012 +0200
@@ -1272,7 +1272,8 @@
     val is_ho = is_type_enc_higher_order type_enc
   in
     t |> need_trueprop ? HOLogic.mk_Trueprop
-      |> (if is_ho then unextensionalize_def else abs_extensionalize_term ctxt)
+      |> (if is_ho then unextensionalize_def
+          else cong_extensionalize_term thy #> abs_extensionalize_term ctxt)
       |> presimplify_term thy
       |> HOLogic.dest_Trueprop
   end