# HG changeset patch
# User blanchet
# Date 1314121825 -7200
# Node ID 860241d0c2a58e89cc81b367103a54f9ba7c6690
# Parent  61fa3dd485b3d57c771f23ceb7d13fe920311cd6
optional reconstructor

diff -r 61fa3dd485b3 -r 860241d0c2a5 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Aug 23 19:49:21 2011 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Aug 23 19:50:25 2011 +0200
@@ -575,8 +575,10 @@
          Metis_Tactics.metis_tac [Metis_Tactics.full_type_enc]
        else if !reconstructor = "metis (no_types)" then
          Metis_Tactics.metis_tac [Metis_Tactics.no_type_enc]
+       else if !reconstructor = "metis" then
+         Metis_Tactics.metis_tac []
        else
-         Metis_Tactics.metis_tac []) ctxt thms
+         K (K (K all_tac))) ctxt thms
     fun apply_reconstructor thms =
       Mirabelle.can_apply timeout (do_reconstructor thms) st