src/HOL/Tools/ATP/atp_translate.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 _ [] t = t
-  | presimplify_term ctxt presimp_consts t =
-    t |> exists_Const (member (op =) presimp_consts o fst) t
-         ? (Skip_Proof.make_thm (Proof_Context.theory_of ctxt)
-            #> Meson.presimplify ctxt
-            #> prop_of)
+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 concealed_bound_name j = atp_weak_prefix ^ string_of_int j
 fun conceal_bounds Ts t =
   subst_bounds (map (Free o apfst concealed_bound_name)
                     (0 upto length Ts - 1 ~~ Ts), t)

       | freeze (Var ((s, i), T)) =
         Free (atp_weak_prefix ^ s ^ "_" ^ string_of_int i, T)
       | freeze t = t
   in t |> exists_subterm is_Var t ? freeze end
 
-fun presimp_prop ctxt presimp_consts role t =
+fun presimp_prop ctxt role t =
   (let
      val thy = Proof_Context.theory_of ctxt
      val t = t |> Envir.beta_eta_contract
                |> transform_elim_prop
                |> 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 presimp_consts
+       |> presimplify_term ctxt
        |> HOLogic.dest_Trueprop
    end
    handle TERM _ => if role = Conjecture then @{term False} else @{term True})
   |> pair role
 

 fun translate_formulas ctxt format prem_kind type_enc lam_trans presimp hyp_ts
                        concl_t facts =
   let
     val thy = Proof_Context.theory_of ctxt
     val trans_lams = trans_lams_from_string ctxt type_enc lam_trans
-    val presimp_consts = Meson.presimplified_consts ctxt
     val fact_ts = facts |> map snd
     (* Remove existing facts from the conjecture, as this can dramatically
        boost an ATP's performance (for some reason). *)
     val hyp_ts =
       hyp_ts

       map (pair prem_kind) hyp_ts @ [(Conjecture, s_not_trueprop concl_t)]
       |> map (apsnd freeze_term)
       |> map2 (pair o rpair Local o string_of_int) (0 upto length hyp_ts)
     val ((conjs, facts), lam_facts) =
       (conjs, facts)
-      |> presimp
-         ? pairself (map (apsnd (uncurry (presimp_prop ctxt presimp_consts))))
+      |> presimp ? pairself (map (apsnd (uncurry (presimp_prop ctxt))))
       |> (if lam_trans = no_lamsN then
             rpair []
           else
             op @
             #> preprocess_abstractions_in_terms trans_lams