# HG changeset patch
# User blanchet
# Date 1292408789 -3600
# Node ID 5ccc40f679d8c2eb0d9047eec25c56326e1f704d
# Parent  626a58993122fcbfbab1e3bb2592cd1207ad3bad
honor "metisFT" in Mirabelle

diff -r 626a58993122 -r 5ccc40f679d8 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- 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