src/HOL/Tools/ATP/atp_translate.ML

--- a/src/HOL/Tools/ATP/atp_translate.ML	Tue May 31 23:39:27 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Wed Jun 01 00:12:38 2011 +0200
@@ -906,6 +906,7 @@
       |> Raw_Simplifier.rewrite_term thy (Meson.unfold_set_const_simps ctxt) []
       |> extensionalize_term ctxt
       |> presimp ? presimplify_term ctxt
+      |> perhaps (try (HOLogic.dest_Trueprop))
       |> introduce_combinators_in_term ctxt kind
   end