src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
changeset 41211 1e2e16bc0077
parent 41199 4698d12dd860
child 41313 a96ac4d180b7
equal deleted inserted replaced
41210:15fbf30288e1 41211:1e2e16bc0077
   224 fun make_formula ctxt eq_as_iff presimp name kind t =
   224 fun make_formula ctxt eq_as_iff presimp name kind t =
   225   let
   225   let
   226     val thy = ProofContext.theory_of ctxt
   226     val thy = ProofContext.theory_of ctxt
   227     val t = t |> Envir.beta_eta_contract
   227     val t = t |> Envir.beta_eta_contract
   228               |> transform_elim_term
   228               |> transform_elim_term
   229               |> atomize_term
   229               |> Object_Logic.atomize_term thy
   230     val need_trueprop = (fastype_of t = HOLogic.boolT)
   230     val need_trueprop = (fastype_of t = HOLogic.boolT)
   231     val t = t |> need_trueprop ? HOLogic.mk_Trueprop
   231     val t = t |> need_trueprop ? HOLogic.mk_Trueprop
   232               |> extensionalize_term
   232               |> extensionalize_term
   233               |> presimp ? presimplify_term thy
   233               |> presimp ? presimplify_term thy
   234               |> perhaps (try (HOLogic.dest_Trueprop))
   234               |> perhaps (try (HOLogic.dest_Trueprop))