make sure "Trueprop" is removed before combinators are added -- the code is fragile in that respect

--- a/src/HOL/Metis_Examples/HO_Reas.thy	Tue May 31 23:39:27 2011 +0200
+++ b/src/HOL/Metis_Examples/HO_Reas.thy	Wed Jun 01 00:12:38 2011 +0200
@@ -48,9 +48,7 @@
 by linarith
 
 lemma "B \<subseteq> C"
-(* FIXME:
 sledgehammer [type_sys = poly_args, max_relevant = 200, expect = some]
-*)
 by (metis B_def C_def int_le_0_imp_le_1 predicate1I)
 
 

--- 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