changeset 43120 | a9c2cdf4ae97 |
parent 43105 | bb0ceef7d39f |
child 43121 | 5df3777f376d |
--- a/src/HOL/Tools/ATP/atp_translate.ML Tue May 31 23:39:27 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_translate.ML Wed Jun 01 00:12:38 2011 +0200 @@ -906,6 +906,7 @@ |> Raw_Simplifier.rewrite_term thy (Meson.unfold_set_const_simps ctxt) [] |> extensionalize_term ctxt |> presimp ? presimplify_term ctxt + |> perhaps (try (HOLogic.dest_Trueprop)) |> introduce_combinators_in_term ctxt kind end