--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon Jun 06 20:36:35 2011 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon Jun 06 20:36:36 2011 +0200
@@ -542,9 +542,9 @@
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