added "smt_triggers" option to experiment with triggers in Sledgehammer;
renamings (for consistency)

--- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Dec 21 01:12:17 2010 +0100
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Dec 21 03:56:51 2010 +0100
@@ -21,7 +21,7 @@
      use_conjecture_for_hypotheses: bool}
 
   (* for experimentation purposes -- do not use in production code *)
-  val e_generate_weights : bool Unsynchronized.ref
+  val e_weights : bool Unsynchronized.ref
   val e_weight_factor : real Unsynchronized.ref
   val e_default_weight : real Unsynchronized.ref
 
@@ -95,13 +95,12 @@
 val tstp_proof_delims =
   ("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation")
 
-val e_generate_weights = Unsynchronized.ref true
+val e_weights = Unsynchronized.ref true
 val e_weight_factor = Unsynchronized.ref 40.0
 val e_default_weight = Unsynchronized.ref 0.5
 
-fun e_weights weights =
-  if !e_generate_weights andalso
-     string_ord (getenv "E_VERSION", "1.2B") <> LESS then
+fun e_weight_arguments weights =
+  if !e_weights andalso string_ord (getenv "E_VERSION", "1.2w") <> LESS then
     "--split-clauses=4 --split-reuse-defs --simul-paramod --forward-context-sr \
     \--destructive-er-aggressive --destructive-er --presat-simplify \
     \--prefer-initial-clauses -tKBO6 -winvfreqrank -c1 -Ginvfreqconjmax -F1 \
@@ -123,7 +122,7 @@
   {exec = ("E_HOME", "eproof"),
    required_execs = [],
    arguments = fn _ => fn timeout => fn weights =>
-     "--tstp-in --tstp-out -l5 " ^ e_weights weights ^ " -tAutoDev \
+     "--tstp-in --tstp-out -l5 " ^ e_weight_arguments weights ^ " -tAutoDev \
      \--silent --cpu-limit=" ^ string_of_int (to_secs (e_bonus ()) timeout),
    has_incomplete_mode = false,
    proof_delims = [tstp_proof_delims],

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Tue Dec 21 01:12:17 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Tue Dec 21 03:56:51 2010 +0100
@@ -10,7 +10,7 @@
   type locality = Sledgehammer_Filter.locality
   type params = Sledgehammer_Provers.params
 
-  val binary_threshold : int Unsynchronized.ref
+  val binary_min_facts : int Unsynchronized.ref
   val filter_used_facts : ''a list -> (''a * 'b) list -> (''a * 'b) list
   val minimize_facts :
     string -> params -> bool -> int -> int -> Proof.state
@@ -86,7 +86,7 @@
    facts as used. In that case, the binary algorithm is much more appropriate.
    We can usually detect the situation by looking at the number of used facts
    reported by the prover. *)
-val binary_threshold = Unsynchronized.ref 20
+val binary_min_facts = Unsynchronized.ref 20
 
 fun filter_used_facts used = filter (member (op =) used o fst)
 
@@ -156,7 +156,7 @@
            |> Time.fromMilliseconds
          val facts = filter_used_facts used_facts facts
          val (min_thms, {message, ...}) =
-           if length facts >= !binary_threshold then
+           if length facts >= !binary_min_facts then
              binary_minimize (do_test new_timeout) facts
            else
              sublinear_minimize (do_test new_timeout) facts ([], result)

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Dec 21 01:12:17 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Dec 21 03:56:51 2010 +0100
@@ -55,6 +55,7 @@
   (* for experimentation purposes -- do not use in production code *)
   val atp_run_twice_threshold : int Unsynchronized.ref
   val atp_first_iter_time_frac : real Unsynchronized.ref
+  val smt_triggers : bool Unsynchronized.ref
   val smt_weights : bool Unsynchronized.ref
   val smt_weight_min_facts : int Unsynchronized.ref
   val smt_min_weight : int Unsynchronized.ref
@@ -65,7 +66,7 @@
   val smt_iter_fact_frac : real Unsynchronized.ref
   val smt_iter_time_frac : real Unsynchronized.ref
   val smt_iter_min_msecs : int Unsynchronized.ref
-  val smt_monomorph_limit : int Unsynchronized.ref
+  val smt_monomorphize_limit : int Unsynchronized.ref
 
   val das_Tool : string
   val select_smt_solver : string -> Proof.context -> Proof.context
@@ -289,7 +290,8 @@
 fun proof_banner auto =
   if auto then "Auto Sledgehammer found a proof" else "Try this command"
 
-val smt_weights = Unsynchronized.ref true
+val smt_triggers = Unsynchronized.ref false
+val smt_weights = Unsynchronized.ref false
 val smt_weight_min_facts = Unsynchronized.ref 20
 
 (* FUDGE *)
@@ -521,7 +523,7 @@
 val smt_iter_fact_frac = Unsynchronized.ref 0.5
 val smt_iter_time_frac = Unsynchronized.ref 0.5
 val smt_iter_min_msecs = Unsynchronized.ref 5000
-val smt_monomorph_limit = Unsynchronized.ref 4
+val smt_monomorphize_limit = Unsynchronized.ref 4
 
 fun smt_filter_loop name ({debug, verbose, overlord, timeout, ...} : params)
                     state i smt_head =
@@ -540,7 +542,8 @@
                         |> (fn (path, base) => path ^ "/" ^ base))
           else
             I)
-      #> Config.put SMT_Config.monomorph_limit (!smt_monomorph_limit)
+      #> Config.put SMT_Config.infer_triggers (!smt_triggers)
+      #> Config.put SMT_Config.monomorph_limit (!smt_monomorphize_limit)
     val state = state |> Proof.map_context repair_context
 
     fun iter timeout iter_num outcome0 time_so_far facts =

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Tue Dec 21 01:12:17 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Tue Dec 21 03:56:51 2010 +0100
@@ -13,7 +13,7 @@
   type params = Sledgehammer_Provers.params
   type prover = Sledgehammer_Provers.prover
 
-  val auto_minimize_threshold : int Unsynchronized.ref
+  val auto_minimize_min_facts : int Unsynchronized.ref
   val get_minimizing_prover : Proof.context -> bool -> string -> prover
   val run_sledgehammer :
     params -> bool -> int -> relevance_override -> (string -> minimize_command)
@@ -42,7 +42,7 @@
    else
      "\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i)))
 
-val auto_minimize_threshold = Unsynchronized.ref (!binary_threshold)
+val auto_minimize_min_facts = Unsynchronized.ref (!binary_min_facts)
 
 fun get_minimizing_prover ctxt auto name (params as {debug, verbose, ...})
         minimize_command
@@ -54,7 +54,7 @@
          else
            let
              val (used_facts, message) =
-               if length used_facts >= !auto_minimize_threshold then
+               if length used_facts >= !auto_minimize_min_facts then
                  minimize_facts name params (not verbose) subgoal subgoal_count
                      state
                      (filter_used_facts used_facts