1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Jul 29 16:54:46 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Jul 29 17:45:22 2010 +0200
     1.3 @@ -232,11 +232,9 @@
     1.4    in aux (maxidx_of_term t + 1) t end
     1.5  
     1.6  fun presimplify_term thy =
     1.7 -  HOLogic.mk_Trueprop
     1.8 -  #> Skip_Proof.make_thm thy
     1.9 +  Skip_Proof.make_thm thy
    1.10    #> Meson.presimplify
    1.11    #> prop_of
    1.12 -  #> HOLogic.dest_Trueprop
    1.13  
    1.14  (* FIXME: Guarantee freshness *)
    1.15  fun concealed_bound_name j = "Sledgehammer" ^ Int.toString j
    1.16 @@ -290,8 +288,10 @@
    1.17      val thy = ProofContext.theory_of ctxt
    1.18      val t = t |> transform_elim_term
    1.19                |> Object_Logic.atomize_term thy
    1.20 +    val t = t |> fastype_of t = HOLogic.boolT ? HOLogic.mk_Trueprop
    1.21                |> extensionalize_term
    1.22                |> presimp ? presimplify_term thy
    1.23 +              |> perhaps (try (HOLogic.dest_Trueprop))
    1.24                |> introduce_combinators_in_term ctxt kind
    1.25      val (combformula, ctypes_sorts) = combformula_for_prop thy t []
    1.26    in

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Thu Jul 29 16:54:46 2010 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Thu Jul 29 17:45:22 2010 +0200
     2.3 @@ -89,7 +89,8 @@
     2.4  
     2.5  val fresh_prefix = "Sledgehammer.Fresh."
     2.6  val flip = Option.map not
     2.7 -val boring_natural_consts = [@{const_name If}]
     2.8 +(* These are typically simplified away by "Meson.presimplify". *)
     2.9 +val boring_consts = [@{const_name If}, @{const_name Let}]
    2.10  
    2.11  fun get_consts_typs thy pos ts =
    2.12    let
    2.13 @@ -139,7 +140,7 @@
    2.14          do_term t0 #> do_formula pos t1  (* theory constant *)
    2.15        | _ => do_term t
    2.16    in
    2.17 -    Symtab.empty |> fold (Symtab.update o rpair []) boring_natural_consts
    2.18 +    Symtab.empty |> fold (Symtab.update o rpair []) boring_consts
    2.19                   |> fold (do_formula pos) ts
    2.20    end
    2.21