src/HOL/Tools/ATP/atp_problem_generate.ML

       | Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>
         if eq_as_iff then do_conn bs AIff NONE t1 NONE t2 else do_term bs t
       | _ => do_term bs t
   in do_formula [] end
 
-fun presimplify_term ctxt t =
-  t |> exists_Const (member (op =) Meson.presimplified_consts o fst) t
-       ? (Skip_Proof.make_thm (Proof_Context.theory_of ctxt)
-          #> Meson.presimplify
-          #> prop_of)
+fun presimplify_term thy t =
+  if exists_Const (member (op =) Meson.presimplified_consts o fst) t then
+    t |> Skip_Proof.make_thm thy
+      |> Meson.presimplify
+      |> prop_of
+  else
+    t
 
 fun is_fun_equality (@{const_name HOL.eq},
                      Type (_, [Type (@{type_name fun}, _), _])) = true
   | is_fun_equality _ = false
 

                |> Object_Logic.atomize_term thy
      val need_trueprop = (fastype_of t = @{typ bool})
    in
      t |> need_trueprop ? HOLogic.mk_Trueprop
        |> extensionalize_term ctxt
-       |> presimplify_term ctxt
+       |> presimplify_term thy
        |> HOLogic.dest_Trueprop
    end
    handle TERM _ => default_formula role)
   |> pair role