src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML

             Method.insert_tac thms THEN'
             Sledgehammer_Tactics.sledgehammer_as_unsound_oracle_tac ctxt)
        else if !reconstructor = "smt" then
          SMT_Solver.smt_tac
        else if full orelse !reconstructor = "metisFT" then
-         Metis_Tactics.old_metisFT_tac
+         Metis_Tactics.new_metisFT_tac
        else
-         Metis_Tactics.old_metis_tac) ctxt thms
+         Metis_Tactics.new_metis_tac []) ctxt thms
     fun apply_reconstructor thms =
       Mirabelle.can_apply timeout (do_reconstructor thms) st
 
     fun with_time (false, t) = "failed (" ^ string_of_int t ^ ")"
       | with_time (true, t) = (change_data id (inc_reconstructor_success m);