src/HOL/ex/sledgehammer_tactics.ML

 structure Sledgehammer_Tactics : SLEDGEHAMMER_TACTICS =
 struct
 
 open Sledgehammer_Filter
 
-fun run_atp override_params relevance_override i n ctxt goal =
+fun run_prover override_params relevance_override i n ctxt goal =
   let
     val chained_ths = [] (* a tactic has no chained ths *)
     val params as {provers, relevance_thresholds, max_relevant, slice, ...} =
       Sledgehammer_Isar.default_params ctxt override_params
     val name = hd provers

   let
     val override_params =
       override_params @
       [("preplay_timeout", "0")]
   in
-    case run_atp override_params relevance_override i i ctxt th of
+    case run_prover override_params relevance_override i i ctxt th of
       SOME facts =>
       Metis_Tactic.metis_tac [] ATP_Problem_Generate.combs_or_liftingN ctxt
           (maps (thms_of_name ctxt) facts) i th
     | NONE => Seq.empty
   end

     val thy = Proof_Context.theory_of ctxt
     val override_params =
       override_params @
       [("preplay_timeout", "0"),
        ("minimize", "false")]
-    val xs = run_atp override_params relevance_override i i ctxt th
+    val xs = run_prover override_params relevance_override i i ctxt th
   in if is_some xs then Skip_Proof.cheat_tac thy th else Seq.empty end
 
 end;