--- 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