added "respect_no_atp" and "convergence" options to Sledgehammer;
these were previously hard-coded in "sledgehammer_fact_filter.ML"

--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Sun Mar 28 18:39:27 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Mon Mar 29 12:01:00 2010 +0200
@@ -14,9 +14,10 @@
      verbose: bool,
      atps: string list,
      full_types: bool,
+     respect_no_atp: bool,
      relevance_threshold: real,
+     convergence: real,
      higher_order: bool option,
-     respect_no_atp: bool,
      follow_defs: bool,
      isar_proof: bool,
      timeout: Time.time,
@@ -56,15 +57,16 @@
 
 (** parameters, problems, results, and provers **)
 
-(* TODO: "theory_const", "blacklist_filter", "convergence" *)
+(* TODO: "theory_const" *)
 type params =
   {debug: bool,
    verbose: bool,
    atps: string list,
    full_types: bool,
+   respect_no_atp: bool,
    relevance_threshold: real,
+   convergence: real,
    higher_order: bool option,
-   respect_no_atp: bool,
    follow_defs: bool,
    isar_proof: bool,
    timeout: Time.time,

--- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Sun Mar 28 18:39:27 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Mon Mar 29 12:01:00 2010 +0200
@@ -159,11 +159,12 @@
 fun generic_tptp_prover
         (name, {command, arguments, failure_strs, max_new_clauses,
                 add_theory_const, supports_isar_proofs})
-        (params as {relevance_threshold, higher_order, follow_defs, isar_proof,
-                    ...}) timeout =
+        (params as {respect_no_atp, relevance_threshold, convergence,
+                    higher_order, follow_defs, isar_proof, ...}) timeout =
   generic_prover
-      (get_relevant_facts relevance_threshold higher_order follow_defs
-                          max_new_clauses add_theory_const)
+      (get_relevant_facts respect_no_atp relevance_threshold convergence
+                          higher_order follow_defs max_new_clauses
+                          add_theory_const)
       (prepare_clauses higher_order false) write_tptp_file command
       (arguments timeout) failure_strs
       (if supports_isar_proofs andalso isar_proof then structured_isar_proof
@@ -212,11 +213,12 @@
 fun generic_dfg_prover
         (name, ({command, arguments, failure_strs, max_new_clauses,
                  add_theory_const, ...} : prover_config))
-        (params as {relevance_threshold, higher_order, follow_defs, ...})
-        timeout =
+        (params as {respect_no_atp, relevance_threshold, convergence,
+                    higher_order, follow_defs, isar_proof, ...}) timeout =
   generic_prover
-      (get_relevant_facts relevance_threshold higher_order follow_defs
-                          max_new_clauses add_theory_const)
+      (get_relevant_facts respect_no_atp relevance_threshold convergence
+                          higher_order follow_defs max_new_clauses
+                          add_theory_const)
       (prepare_clauses higher_order true) write_dfg_file command
       (arguments timeout) failure_strs (metis_lemma_list true) name params;
 

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Sun Mar 28 18:39:27 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Mon Mar 29 12:01:00 2010 +0200
@@ -18,8 +18,8 @@
   val tfree_classes_of_terms : term list -> string list
   val type_consts_of_terms : theory -> term list -> string list
   val get_relevant_facts :
-    real -> bool option -> bool -> int -> bool -> relevance_override
-    -> Proof.context * (thm list * 'a) -> thm list
+    bool -> real -> real -> bool option -> bool -> int -> bool
+    -> relevance_override -> Proof.context * (thm list * 'a) -> thm list
     -> (thm * (string * int)) list
   val prepare_clauses : bool option -> bool -> thm list -> thm list ->
     (thm * (axiom_name * hol_clause_id)) list ->
@@ -41,17 +41,6 @@
    del: Facts.ref list,
    only: bool}
 
-(********************************************************************)
-(* some settings for both background automatic ATP calling procedure*)
-(* and also explicit ATP invocation methods                         *)
-(********************************************************************)
-
-(*** background linkup ***)
-val run_blacklist_filter = true;
-
-(*** relevance filter parameters ***)
-val convergence = 3.2;    (*Higher numbers allow longer inference chains*)
-  
 (***************************************************************)
 (* Relevance Filtering                                         *)
 (***************************************************************)
@@ -263,7 +252,7 @@
       end
   end;
 
-fun relevant_clauses ctxt follow_defs max_new
+fun relevant_clauses ctxt convergence follow_defs max_new
                      (relevance_override as {add, del, only}) thy ctab p
                      rel_consts =
   let val add_thms = maps (ProofContext.get_fact ctxt) add
@@ -277,8 +266,9 @@
             in
               trace_msg (fn () => "relevant this iteration: " ^ Int.toString (length newrels));
                 map #1 newrels @ 
-                relevant_clauses ctxt follow_defs max_new relevance_override thy ctab
-                                 newp rel_consts' (more_rejects @ rejects)
+                relevant_clauses ctxt convergence follow_defs max_new
+                                 relevance_override thy ctab newp rel_consts'
+                                 (more_rejects @ rejects)
             end
         | relevant (newrels, rejects)
                    ((ax as (clsthm as (thm, (name, n)), consts_typs)) :: axs) =
@@ -298,7 +288,7 @@
         relevant ([],[])
     end;
         
-fun relevance_filter ctxt relevance_threshold follow_defs max_new
+fun relevance_filter ctxt relevance_threshold convergence follow_defs max_new
                      add_theory_const relevance_override thy axioms goals = 
   if relevance_threshold > 0.0 then
     let
@@ -309,8 +299,8 @@
         trace_msg (fn () => "Initial constants: " ^
                             commas (Symtab.keys goal_const_tab))
       val relevant =
-        relevant_clauses ctxt follow_defs max_new relevance_override thy
-                         const_tab relevance_threshold goal_const_tab
+        relevant_clauses ctxt convergence follow_defs max_new relevance_override
+                         thy const_tab relevance_threshold goal_const_tab
                          (map (pair_consts_typs_axiom add_theory_const thy)
                               axioms)
     in
@@ -384,7 +374,7 @@
       filter (not o known) c_clauses
   end;
 
-fun all_valid_thms ctxt =
+fun all_valid_thms respect_no_atp ctxt =
   let
     val global_facts = PureThy.facts_of (ProofContext.theory_of ctxt);
     val local_facts = ProofContext.facts_of ctxt;
@@ -404,7 +394,7 @@
           val ths = filter_out bad_for_atp ths0;
         in
           if Facts.is_concealed facts name orelse null ths orelse
-            run_blacklist_filter andalso is_package_def name then I
+            respect_no_atp andalso is_package_def name then I
           else
             (case find_first check_thms [name1, name2, name] of
               NONE => I
@@ -427,13 +417,14 @@
 fun is_multi (a, ths) = length ths > 1 orelse String.isSuffix ".axioms" a;
 
 (*The single theorems go BEFORE the multiple ones. Blacklist is applied to all.*)
-fun name_thm_pairs ctxt =
+fun name_thm_pairs respect_no_atp ctxt =
   let
-    val (mults, singles) = List.partition is_multi (all_valid_thms ctxt)
+    val (mults, singles) =
+      List.partition is_multi (all_valid_thms respect_no_atp ctxt)
     val ps = [] |> fold add_multi_names mults
                 |> fold add_single_names singles
   in
-    if run_blacklist_filter then
+    if respect_no_atp then
       let
         val blacklist = No_ATPs.get ctxt
                         |> map (`Thm.full_prop_of) |> Termtab.make
@@ -447,11 +438,11 @@
       (warning ("No name for theorem " ^ Display.string_of_thm_without_context th); false)
   | check_named _ = true;
 
-fun get_all_lemmas ctxt =
+fun get_all_lemmas respect_no_atp ctxt =
   let val included_thms =
         tap (fn ths => trace_msg
                      (fn () => ("Including all " ^ Int.toString (length ths) ^ " theorems")))
-            (name_thm_pairs ctxt)
+            (name_thm_pairs respect_no_atp ctxt)
   in
     filter check_named included_thms
   end;
@@ -548,18 +539,18 @@
     NONE => forall (Meson.is_fol_term thy) (map prop_of goal_cls)
   | SOME b => not b
 
-fun get_relevant_facts relevance_threshold higher_order follow_defs max_new
-                       add_theory_const relevance_override
-                       (ctxt, (chain_ths, th)) goal_cls =
+fun get_relevant_facts respect_no_atp relevance_threshold convergence
+                       higher_order follow_defs max_new add_theory_const
+                       relevance_override (ctxt, (chain_ths, th)) goal_cls =
   let
     val thy = ProofContext.theory_of ctxt
     val is_FO = is_first_order thy higher_order goal_cls
-    val included_cls = get_all_lemmas ctxt
+    val included_cls = get_all_lemmas respect_no_atp ctxt
       |> cnf_rules_pairs thy |> make_unique
       |> restrict_to_logic thy is_FO
       |> remove_unwanted_clauses
   in
-    relevance_filter ctxt relevance_threshold follow_defs max_new
+    relevance_filter ctxt relevance_threshold convergence follow_defs max_new
                      add_theory_const relevance_override thy included_cls
                      (map prop_of goal_cls)
   end;

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sun Mar 28 18:39:27 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Mar 29 12:01:00 2010 +0200
@@ -40,9 +40,10 @@
 val default_default_params =
   [("debug", "false"),
    ("verbose", "false"),
+   ("respect_no_atp", "true"),
    ("relevance_threshold", "50"),
+   ("convergence", "320"),
    ("higher_order", "smart"),
-   ("respect_no_atp", "true"),
    ("follow_defs", "false"),
    ("isar_proof", "false"),
    ("minimize_timeout", "5 s")]
@@ -50,9 +51,9 @@
 val negated_params =
   [("no_debug", "debug"),
    ("quiet", "verbose"),
+   ("ignore_no_atp", "respect_no_atp"),
    ("partial_types", "full_types"),
    ("first_order", "higher_order"),
-   ("ignore_no_atp", "respect_no_atp"),
    ("dont_follow_defs", "follow_defs"),
    ("metis_proof", "isar_proof")]
 
@@ -119,19 +120,20 @@
     val verbose = debug orelse lookup_bool "verbose"
     val atps = lookup_string "atps" |> space_explode " "
     val full_types = lookup_bool "full_types"
+    val respect_no_atp = lookup_bool "respect_no_atp"
     val relevance_threshold =
       0.01 * Real.fromInt (lookup_int "relevance_threshold")
+    val convergence = 0.01 * Real.fromInt (lookup_int "convergence")
     val higher_order = lookup_bool_option "higher_order"
-    val respect_no_atp = lookup_bool "respect_no_atp"
     val follow_defs = lookup_bool "follow_defs"
     val isar_proof = lookup_bool "isar_proof"
     val timeout = lookup_time "timeout"
     val minimize_timeout = lookup_time "minimize_timeout"
   in
     {debug = debug, verbose = verbose, atps = atps, full_types = full_types,
-     relevance_threshold = relevance_threshold, higher_order = higher_order,
-     respect_no_atp = respect_no_atp, follow_defs = follow_defs,
-     isar_proof = isar_proof, timeout = timeout,
+     respect_no_atp = respect_no_atp, relevance_threshold = relevance_threshold,
+     convergence = convergence, higher_order = higher_order,
+     follow_defs = follow_defs, isar_proof = isar_proof, timeout = timeout,
      minimize_timeout = minimize_timeout}
   end