src/HOL/TPTP/atp_problem_import.ML

   Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt
       ([("debug", if debug then "true" else "false"),
         ("overlord", if overlord then "true" else "false"),
         ("provers", prover),
         ("timeout", string_of_int timeout)] @ override_params)
-      {add = [], del = [], only = true}
+      {add = [(Facts.named (Thm.derivation_name ext), [])],
+       del = [], only = true}
 
 fun sledgehammer_tac ctxt timeout i =
   let
     fun slice overload_params fraq prover =
       SOLVE_TIMEOUT (timeout div fraq) prover

   let
     val (conjs, assms, ctxt) =
       read_tptp_file thy (freeze_problem_consts thy) file_name
     val conj = make_conj assms conjs
   in
-    (can_tac ctxt (sledgehammer_tac ctxt (timeout div 2) 1) conj orelse
-     can_tac ctxt (auto_etc_tac ctxt (timeout div 2) 1) conj orelse
+    (can_tac ctxt (auto_etc_tac ctxt (timeout div 2) 1) conj orelse
+     can_tac ctxt (sledgehammer_tac ctxt (timeout div 2) 1) conj orelse
      can_tac ctxt (atp_tac ctxt [] timeout ATP_Systems.satallaxN 1) conj)
     |> print_szs_from_success conjs
   end
 
 (** Translator between TPTP(-like) file formats **)