# HG changeset patch
# User blanchet
# Date 1306879958 -7200
# Node ID a9c2cdf4ae9754156787a883cd5a1abda2580ac1
# Parent  1286e56edf0654b185db3c2d018137637e2f4277
make sure "Trueprop" is removed before combinators are added -- the code is fragile in that respect

diff -r 1286e56edf06 -r a9c2cdf4ae97 src/HOL/Metis_Examples/HO_Reas.thy
--- 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)
 
 
diff -r 1286e56edf06 -r a9c2cdf4ae97 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