# HG changeset patch
# User blanchet
# Date 1314436941 -7200
# Node ID 3f5fd36352815bff76260d619a86ec159157dac2
# Parent  493781b85dcc73e78c25648708d631285e99c101
beef up sledgehammer_tac in Mirabelle some more

diff -r 493781b85dcc -r 3f5fd3635281 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Sat Aug 27 11:22:11 2011 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Sat Aug 27 11:22:21 2011 +0200
@@ -548,19 +548,10 @@
     | NONE => log (minimize_tag id ^ "failed: " ^ msg)
   end
 
-
-fun e_override_params timeout =
-  [("provers", "e"),
+fun override_params prover type_enc timeout =
+  [("provers", prover),
    ("max_relevant", "0"),
-   ("type_enc", "poly_guards?"),
-   ("sound", "true"),
-   ("slicing", "false"),
-   ("timeout", timeout |> Time.toSeconds |> string_of_int)]
-
-fun vampire_override_params timeout =
-  [("provers", "vampire"),
-   ("max_relevant", "0"),
-   ("type_enc", "poly_tags"),
+   ("type_enc", type_enc),
    ("sound", "true"),
    ("slicing", "false"),
    ("timeout", timeout |> Time.toSeconds |> string_of_int)]
@@ -576,13 +567,14 @@
         val thms = named_thms |> maps snd
         val facts = named_thms |> map (ref_of_str o fst o fst)
         val relevance_override = {add = facts, del = [], only = true}
+        fun sledge_tac prover type_enc =
+          Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt
+            (override_params prover type_enc timeout) relevance_override
       in
         if !reconstructor = "sledgehammer_tac" then
-          Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt
-             (e_override_params timeout) relevance_override
-          ORELSE'
-          Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt
-             (vampire_override_params timeout) relevance_override
+          sledge_tac ATP_Systems.z3_tptpN "simple"
+          ORELSE' sledge_tac ATP_Systems.eN "mono_guards?"
+          ORELSE' sledge_tac ATP_Systems.spassN "poly_tags_uniform"
         else if !reconstructor = "smt" then
           SMT_Solver.smt_tac ctxt thms
         else if full orelse !reconstructor = "metis (full_types)" then