src/HOL/ex/sledgehammer_tactics.ML

   let
     val timeout = Time.fromSeconds 30
   in
     case run_atp false timeout i i ctxt th atp of
       SOME facts =>
-      Metis_Tactics.metis_tac ctxt (maps (thms_of_name ctxt) facts) i th
+      Metis_Tactics.new_metis_tac [] ctxt (maps (thms_of_name ctxt) facts) i th
     | NONE => Seq.empty
   end
 
 fun generic_sledgehammer_as_oracle_tac force_full_types ctxt i th =
   let