src/HOL/Tools/Sledgehammer/sledgehammer.ML

         end
       | aux _ t = t
   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
 fun conceal_bounds Ts t =
   subst_bounds (map (Free o apfst concealed_bound_name)

 fun make_formula ctxt presimp (formula_name, kind, t) =
   let
     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
     FOLFormula {formula_name = formula_name, combformula = combformula,
                 kind = kind, ctypes_sorts = ctypes_sorts}