tuning
authorblanchet
Sat Dec 18 14:02:14 2010 +0100 (2010-12-18)
changeset 41269abe867c29e55
parent 41268 56b7e277fd7d
child 41270 dea60d052923
tuning
src/HOL/Tools/ATP/atp_systems.ML
src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
     1.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Sat Dec 18 13:48:24 2010 +0100
     1.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Sat Dec 18 14:02:14 2010 +0100
     1.3 @@ -204,7 +204,8 @@
     1.4  fun the_system name versions =
     1.5    case get_system name versions of
     1.6      SOME sys => sys
     1.7 -  | NONE => error ("System " ^ quote name ^ " not available at SystemOnTPTP.")
     1.8 +  | NONE => error ("System " ^ quote name ^
     1.9 +                   " is not available at SystemOnTPTP.")
    1.10  
    1.11  val max_remote_secs = 240 (* give Geoff Sutcliffe's servers a break *)
    1.12  
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Sat Dec 18 13:48:24 2010 +0100
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Sat Dec 18 14:02:14 2010 +0100
     2.3 @@ -13,7 +13,7 @@
     2.4    type params = Sledgehammer_Provers.params
     2.5    type prover = Sledgehammer_Provers.prover
     2.6  
     2.7 -  val auto_minimization_threshold : int Unsynchronized.ref
     2.8 +  val auto_minimize_threshold : int Unsynchronized.ref
     2.9    val get_minimizing_prover : Proof.context -> bool -> string -> prover
    2.10    val run_sledgehammer :
    2.11      params -> bool -> int -> relevance_override -> (string -> minimize_command)
    2.12 @@ -42,7 +42,7 @@
    2.13     else
    2.14       "\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i)))
    2.15  
    2.16 -val auto_minimization_threshold = Unsynchronized.ref (!binary_threshold)
    2.17 +val auto_minimize_threshold = Unsynchronized.ref (!binary_threshold)
    2.18  
    2.19  fun get_minimizing_prover ctxt auto name (params as {debug, verbose, ...})
    2.20          minimize_command
    2.21 @@ -54,7 +54,7 @@
    2.22           else
    2.23             let
    2.24               val (used_facts, message) =
    2.25 -               if length used_facts >= !auto_minimization_threshold then
    2.26 +               if length used_facts >= !auto_minimize_threshold then
    2.27                   minimize_facts name params (not verbose) subgoal subgoal_count
    2.28                       state
    2.29                       (filter_used_facts used_facts