honor "metisFT" in Mirabelle

--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Dec 15 11:26:29 2010 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Dec 15 11:26:29 2010 +0100
@@ -331,7 +331,9 @@
 
 (* hack *)
 fun reconstructor_from_msg msg =
-  if String.isSubstring "metis" msg then "metis" else "smt"
+  if String.isSubstring "metisFT" msg then "metisFT"
+  else if String.isSubstring "metis" msg then "metis"
+  else "smt"
 
 local
 
@@ -482,9 +484,12 @@
     ({pre=st, timeout, log, pos, ...}: Mirabelle.run_args) =
   let
     fun do_reconstructor thms ctxt =
-      (if !reconstructor = "smt" then SMT_Solver.smt_tac
-       else if full then Metis_Tactics.metisFT_tac
-       else Metis_Tactics.metis_tac) ctxt thms
+      (if !reconstructor = "smt" then
+         SMT_Solver.smt_tac
+       else if full orelse !reconstructor = "metisFT" then
+         Metis_Tactics.metisFT_tac
+       else
+         Metis_Tactics.metis_tac) ctxt thms
     fun apply_reconstructor thms =
       Mirabelle.can_apply timeout (do_reconstructor thms) st