# HG changeset patch
# User blanchet
# Date 1304369535 -7200
# Node ID f5b4b9d4acda69fa36f278c6bdd28c84a3e84a8c
# Parent  2cd4e64638424da4adb85113bae9ae6f6db1857a
tuning

diff -r 2cd4e6463842 -r f5b4b9d4acda src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon May 02 22:52:15 2011 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon May 02 22:52:15 2011 +0200
@@ -362,7 +362,7 @@
       st |> Proof.map_context
                 (change_dir dir
                  #> Config.put Sledgehammer_Provers.measure_run_time true)
-    val params as {type_sys, relevance_thresholds, max_relevant, slicing, ...} =
+    val params as {relevance_thresholds, max_relevant, slicing, ...} =
       Sledgehammer_Isar.default_params ctxt
           [("verbose", "true"),
            ("type_sys", type_sys),
diff -r 2cd4e6463842 -r f5b4b9d4acda src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Mon May 02 22:52:15 2011 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Mon May 02 22:52:15 2011 +0200
@@ -112,7 +112,7 @@
          val {context = ctxt, facts, goal} = Proof.goal pre
          val prover = AList.lookup (op =) args "prover"
                       |> the_default default_prover
-         val {relevance_thresholds, type_sys, max_relevant, slicing, ...} =
+         val {relevance_thresholds, max_relevant, slicing, ...} =
            Sledgehammer_Isar.default_params ctxt args
          val default_max_relevant =
            Sledgehammer_Provers.default_max_relevant_for_prover ctxt slicing
diff -r 2cd4e6463842 -r f5b4b9d4acda src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon May 02 22:52:15 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon May 02 22:52:15 2011 +0200
@@ -642,7 +642,6 @@
                            timeout, slicing, ...} : params)
                     state i smt_filter =
   let
-    val ctxt = Proof.context_of state
     val max_slices = if slicing then !smt_max_slices else 1
     val repair_context =
       select_smt_solver name
diff -r 2cd4e6463842 -r f5b4b9d4acda src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Mon May 02 22:52:15 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Mon May 02 22:52:15 2011 +0200
@@ -164,9 +164,8 @@
 
 val auto_max_relevant_divisor = 2 (* FUDGE *)
 
-fun run_sledgehammer (params as {debug, blocking, provers, type_sys,
-                                 relevance_thresholds, max_relevant, slicing,
-                                 timeout, ...})
+fun run_sledgehammer (params as {debug, blocking, provers, relevance_thresholds,
+                                 max_relevant, slicing, timeout, ...})
         auto i (relevance_override as {only, ...}) minimize_command state =
   if null provers then
     error "No prover is set."
diff -r 2cd4e6463842 -r f5b4b9d4acda src/HOL/ex/sledgehammer_tactics.ML
--- a/src/HOL/ex/sledgehammer_tactics.ML	Mon May 02 22:52:15 2011 +0200
+++ b/src/HOL/ex/sledgehammer_tactics.ML	Mon May 02 22:52:15 2011 +0200
@@ -18,7 +18,7 @@
 fun run_atp force_full_types timeout i n ctxt goal name =
   let
     val chained_ths = [] (* a tactic has no chained ths *)
-    val params as {type_sys, relevance_thresholds, max_relevant, slicing, ...} =
+    val params as {relevance_thresholds, max_relevant, slicing, ...} =
       ((if force_full_types then [("full_types", "true")] else [])
        @ [("timeout", string_of_int (Time.toSeconds timeout))])
        (* @ [("overlord", "true")] *)
diff -r 2cd4e6463842 -r f5b4b9d4acda src/HOL/ex/tptp_export.ML
--- a/src/HOL/ex/tptp_export.ML	Mon May 02 22:52:15 2011 +0200
+++ b/src/HOL/ex/tptp_export.ML	Mon May 02 22:52:15 2011 +0200
@@ -23,7 +23,7 @@
 
 fun facts_of thy =
   Sledgehammer_Filter.all_facts (ProofContext.init_global thy) Symtab.empty
-      true Sledgehammer_Provers.atp_relevance_fudge [] []
+                                true [] []
 
 fun fold_body_thms f =
   let