# 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