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