# HG changeset patch
# User blanchet
# Date 1280418322 -7200
# Node ID 0508ff84036fe1f484db49389a32a216ab6dd145
# Parent  fe51c098b0ab5cb1fd16c19aec4ffd51e526e2c4
work around atomization failures

diff -r fe51c098b0ab -r 0508ff84036f src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Jul 29 16:54:46 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Jul 29 17:45:22 2010 +0200
@@ -232,11 +232,9 @@
   in aux (maxidx_of_term t + 1) t end
 
 fun presimplify_term thy =
-  HOLogic.mk_Trueprop
-  #> Skip_Proof.make_thm thy
+  Skip_Proof.make_thm thy
   #> Meson.presimplify
   #> prop_of
-  #> HOLogic.dest_Trueprop
 
 (* FIXME: Guarantee freshness *)
 fun concealed_bound_name j = "Sledgehammer" ^ Int.toString j
@@ -290,8 +288,10 @@
     val thy = ProofContext.theory_of ctxt
     val t = t |> transform_elim_term
               |> Object_Logic.atomize_term thy
+    val t = t |> fastype_of t = HOLogic.boolT ? HOLogic.mk_Trueprop
               |> extensionalize_term
               |> presimp ? presimplify_term thy
+              |> perhaps (try (HOLogic.dest_Trueprop))
               |> introduce_combinators_in_term ctxt kind
     val (combformula, ctypes_sorts) = combformula_for_prop thy t []
   in
diff -r fe51c098b0ab -r 0508ff84036f src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Thu Jul 29 16:54:46 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Thu Jul 29 17:45:22 2010 +0200
@@ -89,7 +89,8 @@
 
 val fresh_prefix = "Sledgehammer.Fresh."
 val flip = Option.map not
-val boring_natural_consts = [@{const_name If}]
+(* These are typically simplified away by "Meson.presimplify". *)
+val boring_consts = [@{const_name If}, @{const_name Let}]
 
 fun get_consts_typs thy pos ts =
   let
@@ -139,7 +140,7 @@
         do_term t0 #> do_formula pos t1  (* theory constant *)
       | _ => do_term t
   in
-    Symtab.empty |> fold (Symtab.update o rpair []) boring_natural_consts
+    Symtab.empty |> fold (Symtab.update o rpair []) boring_consts
                  |> fold (do_formula pos) ts
   end