equal
deleted
inserted
replaced
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)) |