Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
optional reconstructor
authorblanchet
Tue, 23 Aug 2011 19:50:25 +0200
changeset 44447 860241d0c2a5
parent 44432 61fa3dd485b3
child 44448 04bd6a9307c6
optional reconstructor
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle