src/HOL/Tools/ATP/atp_translate.ML

   in
     t |> need_trueprop ? HOLogic.mk_Trueprop
       |> 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
 
 (* making fact and conjecture formulas *)
 fun make_formula thy format type_sys eq_as_iff name loc kind t =