# HG changeset patch
# User blanchet
# Date 1314117725 -7200
# Node ID c6f0490d432fc311bcdb8d26ebb992aeb7d3afb9
# Parent  e5506cfe1b5a50ca76bbc310cc375523e48bf841
beef up "sledgehammer_tac" reconstructor

diff -r e5506cfe1b5a -r c6f0490d432f src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Aug 23 18:42:05 2011 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Aug 23 18:42:05 2011 +0200
@@ -543,6 +543,18 @@
   end
 
 
+val e_override_params =
+  [("provers", "e"),
+   ("type_enc", "poly_guards?"),
+   ("sound", "true"),
+   ("slicing", "false")]
+
+val vampire_override_params =
+  [("provers", "vampire"),
+   ("type_enc", "poly_tags"),
+   ("sound", "true"),
+   ("slicing", "false")]
+
 fun run_reconstructor trivial full m name reconstructor named_thms id
     ({pre=st, timeout, log, pos, ...}: Mirabelle.run_args) =
   let
@@ -550,7 +562,11 @@
       (if !reconstructor = "sledgehammer_tac" then
          (fn ctxt => fn thms =>
             Method.insert_tac thms THEN'
-            Sledgehammer_Tactics.sledgehammer_as_unsound_oracle_tac ctxt)
+            (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt
+                 e_override_params
+             ORELSE'
+             Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt
+                 vampire_override_params))
        else if !reconstructor = "smt" then
          SMT_Solver.smt_tac
        else if full orelse !reconstructor = "metis (full_types)" then