# HG changeset patch
# User blanchet
# Date 1304374222 -7200
# Node ID 4781fcd53572d9f361a0f2ab1c16e3e091200b1a
# Parent  242bc53b98e5909bba6ac2cc368029b73c19e7d1
replaced some Unsynchronized.refs with Config.Ts

diff -r 242bc53b98e5 -r 4781fcd53572 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Mon May 02 23:01:22 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue May 03 00:10:22 2011 +0200
@@ -14,26 +14,23 @@
   type atp_config =
     {exec : string * string,
      required_execs : (string * string) list,
-     arguments : int -> Time.time -> (unit -> (string * real) list) -> string,
+     arguments :
+       Proof.context -> int -> Time.time -> (unit -> (string * real) list)
+       -> string,
      proof_delims : (string * string) list,
      known_failures : (failure * string) list,
      hypothesis_kind : formula_kind,
      formats : format list,
-     best_slices : unit -> (real * (bool * int)) list,
+     best_slices : Proof.context -> (real * (bool * int)) list,
      best_type_systems : string list}
 
-  datatype e_weight_method =
-    E_Slices | E_Auto | E_Fun_Weight | E_Sym_Offset_Weight
-
-  (* for experimentation purposes -- do not use in production code *)
-  val e_weight_method : e_weight_method Unsynchronized.ref
-  val e_default_fun_weight : real Unsynchronized.ref
-  val e_fun_weight_base : real Unsynchronized.ref
-  val e_fun_weight_span : real Unsynchronized.ref
-  val e_default_sym_offs_weight : real Unsynchronized.ref
-  val e_sym_offs_weight_base : real Unsynchronized.ref
-  val e_sym_offs_weight_span : real Unsynchronized.ref
-  (* end *)
+  val e_weight_method : string Config.T
+  val e_default_fun_weight : real Config.T
+  val e_fun_weight_base : real Config.T
+  val e_fun_weight_span : real Config.T
+  val e_default_sym_offs_weight : real Config.T
+  val e_sym_offs_weight_base : real Config.T
+  val e_sym_offs_weight_span : real Config.T
   val eN : string
   val spassN : string
   val vampireN : string
@@ -44,8 +41,8 @@
   val remote_prefix : string
   val remote_atp :
     string -> string -> string list -> (string * string) list
-    -> (failure * string) list -> formula_kind -> format list -> (unit -> int)
-    -> string list -> string * atp_config
+    -> (failure * string) list -> formula_kind -> format list
+    -> (Proof.context -> int) -> string list -> string * atp_config
   val add_atp : string * atp_config -> theory -> theory
   val get_atp : theory -> string -> atp_config
   val supported_atps : theory -> string list
@@ -65,12 +62,14 @@
 type atp_config =
   {exec : string * string,
    required_execs : (string * string) list,
-   arguments : int -> Time.time -> (unit -> (string * real) list) -> string,
+   arguments :
+     Proof.context -> int -> Time.time -> (unit -> (string * real) list)
+     -> string,
    proof_delims : (string * string) list,
    known_failures : (failure * string) list,
    hypothesis_kind : formula_kind,
    formats : format list,
-   best_slices : unit -> (real * (bool * int)) list,
+   best_slices : Proof.context -> (real * (bool * int)) list,
    best_type_systems : string list}
 
 val known_perl_failures =
@@ -113,31 +112,41 @@
 val tstp_proof_delims =
   ("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation")
 
-datatype e_weight_method =
-  E_Slices | E_Auto | E_Fun_Weight | E_Sym_Offset_Weight
+val e_slicesN = "slices"
+val e_autoN = "auto"
+val e_fun_weightN = "fun_weight"
+val e_sym_offset_weightN = "sym_offset_weight"
 
-val e_weight_method = Unsynchronized.ref E_Slices
+val e_weight_method =
+  Attrib.setup_config_string @{binding atp_e_weight_method} (K e_slicesN)
 (* FUDGE *)
-val e_default_fun_weight = Unsynchronized.ref 20.0
-val e_fun_weight_base = Unsynchronized.ref 0.0
-val e_fun_weight_span = Unsynchronized.ref 40.0
-val e_default_sym_offs_weight = Unsynchronized.ref 1.0
-val e_sym_offs_weight_base = Unsynchronized.ref ~20.0
-val e_sym_offs_weight_span = Unsynchronized.ref 60.0
+val e_default_fun_weight =
+  Attrib.setup_config_real @{binding atp_e_default_fun_weight} (K 20.0)
+val e_fun_weight_base =
+  Attrib.setup_config_real @{binding atp_e_fun_weight_base} (K 0.0)
+val e_fun_weight_span =
+  Attrib.setup_config_real @{binding atp_e_fun_weight_span} (K 40.0)
+val e_default_sym_offs_weight =
+  Attrib.setup_config_real @{binding atp_e_default_sym_offs_weight} (K 1.0)
+val e_sym_offs_weight_base =
+  Attrib.setup_config_real @{binding atp_e_sym_offs_weight_base} (K ~20.0)
+val e_sym_offs_weight_span =
+  Attrib.setup_config_real @{binding atp_e_sym_offs_weight_span} (K 60.0)
 
 fun e_weight_method_case method fw sow =
-  case method of
-    E_Auto => raise Fail "Unexpected \"E_Auto\""
-  | E_Fun_Weight => fw
-  | E_Sym_Offset_Weight => sow
+  if method = e_fun_weightN then fw
+  else if method = e_sym_offset_weightN then sow
+  else raise Fail ("unexpected" ^ quote method)
 
-fun scaled_e_weight method w =
-  w * e_weight_method_case method (!e_fun_weight_span) (!e_sym_offs_weight_span)
-  + e_weight_method_case method (!e_fun_weight_base) (!e_sym_offs_weight_base)
+fun scaled_e_weight ctxt method w =
+  w * Config.get ctxt
+          (e_weight_method_case method e_fun_weight_span e_sym_offs_weight_span)
+  + Config.get ctxt
+        (e_weight_method_case method e_fun_weight_base e_sym_offs_weight_base)
   |> Real.ceil |> signed_string_of_int
 
-fun e_weight_arguments method weights =
-  if method = E_Auto then
+fun e_weight_arguments ctxt method weights =
+  if method = e_autoN then
     "-xAutoDev"
   else
     "--split-clauses=4 --split-reuse-defs --simul-paramod --forward-context-sr \
@@ -146,37 +155,40 @@
     \--delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred \
     \-H'(4*" ^ e_weight_method_case method "FunWeight" "SymOffsetWeight" ^
     "(SimulateSOS, " ^
-    (e_weight_method_case method (!e_default_fun_weight)
-                                 (!e_default_sym_offs_weight)
-     |> Real.ceil |> signed_string_of_int) ^
+    (e_weight_method_case method e_default_fun_weight e_default_sym_offs_weight
+     |> Config.get ctxt |> Real.ceil |> signed_string_of_int) ^
     ",20,1.5,1.5,1" ^
-    (weights () |> map (fn (s, w) => "," ^ s ^ ":" ^ scaled_e_weight method w)
-                |> implode) ^
+    (weights ()
+     |> map (fn (s, w) => "," ^ s ^ ":" ^ scaled_e_weight ctxt method w)
+     |> implode) ^
     "),3*ConjectureGeneralSymbolWeight(PreferNonGoals,200,100,200,50,50,1,100,\
     \1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*\
     \FIFOWeight(PreferProcessed))'"
 
 fun is_old_e_version () = (string_ord (getenv "E_VERSION", "1.2w") = LESS)
 
-fun effective_e_weight_method () =
-  if is_old_e_version () then E_Auto else !e_weight_method
+fun effective_e_weight_method ctxt =
+  if is_old_e_version () then e_autoN else Config.get ctxt e_weight_method
 
 (* The order here must correspond to the order in "e_config" below. *)
-fun method_for_slice slice =
-  case effective_e_weight_method () of
-    E_Slices => (case slice of
-                   0 => E_Sym_Offset_Weight
-                 | 1 => E_Auto
-                 | 2 => E_Fun_Weight
-                 | _ => raise Fail "no such slice")
-  | method => method
+fun method_for_slice ctxt slice =
+  let val method = effective_e_weight_method ctxt in
+    if method = e_slicesN then
+      case slice of
+        0 => e_sym_offset_weightN
+      | 1 => e_autoN
+      | 2 => e_fun_weightN
+      | _ => raise Fail "no such slice"
+    else
+      method
+  end
 
 val e_config : atp_config =
   {exec = ("E_HOME", "eproof"),
    required_execs = [],
-   arguments = fn slice => fn timeout => fn weights =>
+   arguments = fn ctxt => fn slice => fn timeout => fn weights =>
      "--tstp-in --tstp-out -l5 " ^
-     e_weight_arguments (method_for_slice slice) weights ^
+     e_weight_arguments ctxt (method_for_slice ctxt slice) weights ^
      " -tAutoDev --silent --cpu-limit=" ^
      string_of_int (to_secs (e_bonus ()) timeout),
    proof_delims = [tstp_proof_delims],
@@ -191,11 +203,11 @@
       (OutOfResources, "SZS status ResourceOut")],
    hypothesis_kind = Conjecture,
    formats = [Fof],
-   best_slices = fn () =>
-     if effective_e_weight_method () = E_Slices then
-       [(0.33333, (true, 100 (* FUDGE *))) (* E_Sym_Offset_Weight *),
-        (0.33333, (true, 1000 (* FUDGE *))) (* E_Auto *),
-        (0.33334, (true, 200 (* FUDGE *))) (* E_Fun_Weight *)]
+   best_slices = fn ctxt =>
+     if effective_e_weight_method ctxt = e_slicesN then
+       [(0.33333, (true, 100 (* FUDGE *))) (* sym_offset_weight *),
+        (0.33333, (true, 1000 (* FUDGE *))) (* auto *),
+        (0.33334, (true, 200 (* FUDGE *))) (* fun_weight *)]
      else
        [(1.0, (true, 250 (* FUDGE *)))],
    best_type_systems = ["const_args", "mangled_preds"]}
@@ -210,7 +222,7 @@
 val spass_config : atp_config =
   {exec = ("ISABELLE_ATP", "scripts/spass"),
    required_execs = [("SPASS_HOME", "SPASS"), ("SPASS_HOME", "tptp2dfg")],
-   arguments = fn slice => fn timeout => fn _ =>
+   arguments = fn _ => fn slice => fn timeout => fn _ =>
      ("-Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \
       \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_secs 0 timeout))
      |> slice = 0 ? prefix "-SOS=1 ",
@@ -239,7 +251,7 @@
 val vampire_config : atp_config =
   {exec = ("VAMPIRE_HOME", "vampire"),
    required_execs = [],
-   arguments = fn slice => fn timeout => fn _ =>
+   arguments = fn _ => fn slice => fn timeout => fn _ =>
      (* This would work too but it's less tested: "--proof tptp " ^ *)
      "--mode casc -t " ^ string_of_int (to_secs 0 timeout) ^
      " --thanks \"Andrei and Krystof\" --input_file"
@@ -275,7 +287,7 @@
 val z3_atp_config : atp_config =
   {exec = ("Z3_HOME", "z3"),
    required_execs = [],
-   arguments = fn _ => fn timeout => fn _ =>
+   arguments = fn _ => fn _ => fn timeout => fn _ =>
      "MBQI=true -p -t:" ^ string_of_int (to_secs 0 timeout),
    proof_delims = [],
    known_failures =
@@ -329,7 +341,7 @@
                   : atp_config =
   {exec = ("ISABELLE_ATP", "scripts/remote_atp"),
    required_execs = [],
-   arguments = fn _ => fn timeout => fn _ =>
+   arguments = fn _ => fn _ => fn timeout => fn _ =>
      " -t " ^ string_of_int (Int.min (max_remote_secs, (to_secs 0 timeout)))
      ^ " -s " ^ the_system system_name system_versions,
    proof_delims = insert (op =) tstp_proof_delims proof_delims,
@@ -340,7 +352,7 @@
       (TimedOut, "says Timeout")],
    hypothesis_kind = hypothesis_kind,
    formats = formats,
-   best_slices = fn () => [(1.0, (false, best_max_relevant ()))],
+   best_slices = fn ctxt => [(1.0, (false, best_max_relevant ctxt))],
    best_type_systems = best_type_systems}
 
 fun int_average f xs = fold (Integer.add o f) xs 0 div length xs
diff -r 242bc53b98e5 -r 4781fcd53572 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Mon May 02 23:01:22 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Tue May 03 00:10:22 2011 +0200
@@ -23,7 +23,7 @@
 
   type translated_formula
 
-  val readable_names : bool Unsynchronized.ref
+  val readable_names : bool Config.T
   val fact_prefix : string
   val conjecture_prefix : string
   val predicator_base : string
@@ -63,7 +63,8 @@
    names. Also, the logic for generating legal SNARK sort names is only
    implemented for readable names. Finally, readable names are, well, more
    readable. For these reason, they are enabled by default. *)
-val readable_names = Unsynchronized.ref true
+val readable_names =
+  Attrib.setup_config_bool @{binding sledgehammer_atp_readable_names} (K true)
 
 val type_decl_prefix = "type_"
 val sym_decl_prefix = "sym_"
@@ -983,7 +984,8 @@
                   map decl_line_for_tff_type (tff_types_in_problem problem))
           else
             I)
-    val (problem, pool) = problem |> nice_atp_problem (!readable_names)
+    val (problem, pool) =
+      problem |> nice_atp_problem (Config.get ctxt readable_names)
   in
     (problem,
      case pool of SOME the_pool => snd the_pool | NONE => Symtab.empty,
diff -r 242bc53b98e5 -r 4781fcd53572 src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Mon May 02 23:01:22 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Tue May 03 00:10:22 2011 +0200
@@ -35,7 +35,7 @@
      del : (Facts.ref * Attrib.src list) list,
      only : bool}
 
-  val trace : bool Unsynchronized.ref
+  val trace : bool Config.T
   val is_global_locality : locality -> bool
   val fact_from_ref :
     Proof.context -> unit Symtab.table -> thm list
@@ -59,8 +59,9 @@
 
 open Sledgehammer_Util
 
-val trace = Unsynchronized.ref false
-fun trace_msg msg = if !trace then tracing (msg ()) else ()
+val trace =
+  Attrib.setup_config_bool @{binding sledgehammer_filter_trace} (K false)
+fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
 
 (* experimental features *)
 val respect_no_atp = true
@@ -496,7 +497,7 @@
 type annotated_thm =
   (((unit -> string) * locality) * thm) * (string * ptype) list
 
-fun take_most_relevant max_relevant remaining_max
+fun take_most_relevant ctxt max_relevant remaining_max
         ({max_imperfect, max_imperfect_exp, ...} : relevance_fudge) 
         (candidates : (annotated_thm * real) list) =
   let
@@ -510,7 +511,7 @@
     val ((accepts, more_rejects), rejects) =
       chop max_imperfect imperfect |>> append perfect |>> chop remaining_max
   in
-    trace_msg (fn () =>
+    trace_msg ctxt (fn () =>
         "Actually passed (" ^ string_of_int (length accepts) ^ " of " ^
         string_of_int (length candidates) ^ "): " ^
         (accepts |> map (fn ((((name, _), _), _), weight) =>
@@ -572,7 +573,8 @@
           | relevant candidates rejects [] =
             let
               val (accepts, more_rejects) =
-                take_most_relevant max_relevant remaining_max fudge candidates
+                take_most_relevant ctxt max_relevant remaining_max fudge
+                                   candidates
               val rel_const_tab' =
                 rel_const_tab
                 |> fold (add_pconst_to_table false) (maps (snd o fst) accepts)
@@ -594,7 +596,7 @@
                       * Math.pow (decay, Real.fromInt (length accepts))
               val remaining_max = remaining_max - length accepts
             in
-              trace_msg (fn () => "New or updated constants: " ^
+              trace_msg ctxt (fn () => "New or updated constants: " ^
                   commas (rel_const_tab' |> Symtab.dest
                           |> subtract (op =) (rel_const_tab |> Symtab.dest)
                           |> map string_for_hyper_pconst));
@@ -621,7 +623,7 @@
                 relevant candidates ((ax, weight) :: rejects) hopeful
             end
         in
-          trace_msg (fn () =>
+          trace_msg ctxt (fn () =>
               "ITERATION " ^ string_of_int j ^ ": current threshold: " ^
               Real.toString threshold ^ ", constants: " ^
               commas (rel_const_tab |> Symtab.dest
@@ -640,7 +642,7 @@
           |> (fn accepts =>
                  accepts |> needs_ext is_built_in_const accepts
                             ? add_facts @{thms ext})
-          |> tap (fn accepts => trace_msg (fn () =>
+          |> tap (fn accepts => trace_msg ctxt (fn () =>
                       "Total relevant: " ^ string_of_int (length accepts)))
   end
 
@@ -920,8 +922,8 @@
       |> rearrange_facts ctxt (respect_no_atp andalso not only)
       |> uniquify
   in
-    trace_msg (fn () => "Considering " ^ string_of_int (length facts) ^
-                        " facts");
+    trace_msg ctxt (fn () => "Considering " ^ string_of_int (length facts) ^
+                             " facts");
     (if only orelse threshold1 < 0.0 then
        facts
      else if threshold0 > 1.0 orelse threshold0 > threshold1 orelse
diff -r 242bc53b98e5 -r 4781fcd53572 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Mon May 02 23:01:22 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Tue May 03 00:10:22 2011 +0200
@@ -10,7 +10,7 @@
   type locality = Sledgehammer_Filter.locality
   type params = Sledgehammer_Provers.params
 
-  val binary_min_facts : int Unsynchronized.ref
+  val binary_min_facts : int Config.T
   val filter_used_facts : ''a list -> (''a * 'b) list -> (''a * 'b) list
   val minimize_facts :
     string -> params -> bool option -> bool -> int -> int -> Proof.state
@@ -90,7 +90,9 @@
    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_min_facts = Unsynchronized.ref 20
+val binary_min_facts =
+  Attrib.setup_config_int @{binding sledgehammer_minimize_binary_min_facts}
+                          (K 20)
 
 fun filter_used_facts used = filter (member (op =) used o fst)
 
@@ -164,7 +166,7 @@
            |> Time.fromMilliseconds
          val facts = filter_used_facts used_facts facts
          val (min_thms, {message, ...}) =
-           if length facts >= !binary_min_facts then
+           if length facts >= Config.get ctxt binary_min_facts then
              binary_minimize (do_test new_timeout) facts
            else
              sublinear_minimize (do_test new_timeout) facts ([], result)
diff -r 242bc53b98e5 -r 4781fcd53572 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon May 02 23:01:22 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue May 03 00:10:22 2011 +0200
@@ -56,19 +56,17 @@
 
   type prover = params -> minimize_command -> prover_problem -> prover_result
 
-  (* for experimentation purposes -- do not use in production code *)
-  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
-  val smt_max_weight : int Unsynchronized.ref
-  val smt_max_weight_index : int Unsynchronized.ref
+  val smt_triggers : bool Config.T
+  val smt_weights : bool Config.T
+  val smt_weight_min_facts : int Config.T
+  val smt_min_weight : int Config.T
+  val smt_max_weight : int Config.T
+  val smt_max_weight_index : int Config.T
   val smt_weight_curve : (int -> int) Unsynchronized.ref
-  val smt_max_slices : int Unsynchronized.ref
-  val smt_slice_fact_frac : real Unsynchronized.ref
-  val smt_slice_time_frac : real Unsynchronized.ref
-  val smt_slice_min_secs : int Unsynchronized.ref
-  (* end *)
+  val smt_max_slices : int Config.T
+  val smt_slice_fact_frac : real Config.T
+  val smt_slice_time_frac : real Config.T
+  val smt_slice_min_secs : int Config.T
   val das_Tool : string
   val select_smt_solver : string -> Proof.context -> Proof.context
   val is_smt_prover : Proof.context -> string -> bool
@@ -84,11 +82,11 @@
   val problem_prefix : string Config.T
   val measure_run_time : bool Config.T
   val weight_smt_fact :
-    theory -> int -> ((string * locality) * thm) * int
+    Proof.context -> int -> ((string * locality) * thm) * int
     -> (string * locality) * (int option * thm)
   val untranslated_fact : prover_fact -> (string * locality) * thm
   val smt_weighted_fact :
-    theory -> int -> prover_fact * int
+    Proof.context -> int -> prover_fact * int
     -> (string * locality) * (int option * thm)
   val supported_provers : Proof.context -> unit
   val kill_provers : unit -> unit
@@ -138,7 +136,7 @@
       SMT_Solver.default_max_relevant ctxt name
     else
       fold (Integer.max o snd o snd o snd)
-           (get_slices slicing (#best_slices (get_atp thy name) ())) 0
+           (get_slices slicing (#best_slices (get_atp thy name) ctxt)) 0
   end
 
 (* These are either simplified away by "Meson.presimplify" (most of the time) or
@@ -289,35 +287,49 @@
 fun proof_banner auto =
   if auto then "Auto Sledgehammer found a proof" else "Try this command"
 
-val smt_triggers = Unsynchronized.ref true
-val smt_weights = Unsynchronized.ref true
-val smt_weight_min_facts = Unsynchronized.ref 20
+val smt_triggers =
+  Attrib.setup_config_bool @{binding sledgehammer_smt_triggers} (K true)
+val smt_weights =
+  Attrib.setup_config_bool @{binding sledgehammer_smt_weights} (K true)
+val smt_weight_min_facts =
+  Attrib.setup_config_int @{binding sledgehammer_smt_weight_min_facts} (K 20)
 
 (* FUDGE *)
-val smt_min_weight = Unsynchronized.ref 0
-val smt_max_weight = Unsynchronized.ref 10
-val smt_max_weight_index = Unsynchronized.ref 200
+val smt_min_weight =
+  Attrib.setup_config_int @{binding sledgehammer_smt_min_weight} (K 0)
+val smt_max_weight =
+  Attrib.setup_config_int @{binding sledgehammer_smt_max_weight} (K 10)
+val smt_max_weight_index =
+  Attrib.setup_config_int @{binding sledgehammer_smt_max_weight_index} (K 200)
 val smt_weight_curve = Unsynchronized.ref (fn x : int => x * x)
 
-fun smt_fact_weight j num_facts =
-  if !smt_weights andalso num_facts >= !smt_weight_min_facts then
-    SOME (!smt_max_weight
-          - (!smt_max_weight - !smt_min_weight + 1)
-            * !smt_weight_curve (Int.max (0, !smt_max_weight_index - j - 1))
-            div !smt_weight_curve (!smt_max_weight_index))
+fun smt_fact_weight ctxt j num_facts =
+  if Config.get ctxt smt_weights andalso
+     num_facts >= Config.get ctxt smt_weight_min_facts then
+    let
+      val min = Config.get ctxt smt_min_weight
+      val max = Config.get ctxt smt_max_weight
+      val max_index = Config.get ctxt smt_max_weight_index
+      val curve = !smt_weight_curve
+    in
+      SOME (max - (max - min + 1) * curve (Int.max (0, max_index - j - 1))
+            div curve max_index)
+    end
   else
     NONE
 
-fun weight_smt_fact thy num_facts ((info, th), j) =
-  (info, (smt_fact_weight j num_facts, th |> Thm.transfer thy))
+fun weight_smt_fact ctxt num_facts ((info, th), j) =
+  let val thy = Proof_Context.theory_of ctxt in
+    (info, (smt_fact_weight ctxt j num_facts, th |> Thm.transfer thy))
+  end
 
 fun untranslated_fact (Untranslated_Fact p) = p
   | untranslated_fact (SMT_Weighted_Fact (info, (_, th))) = (info, th)
 fun atp_translated_fact ctxt fact =
     translate_atp_fact ctxt false (untranslated_fact fact)
 fun smt_weighted_fact _ _ (SMT_Weighted_Fact p, _) = p
-  | smt_weighted_fact thy num_facts (fact, j) =
-    (untranslated_fact fact, j) |> weight_smt_fact thy num_facts
+  | smt_weighted_fact ctxt num_facts (fact, j) =
+    (untranslated_fact fact, j) |> weight_smt_fact ctxt num_facts
 
 fun overlord_file_location_for_prover prover =
   (getenv "ISABELLE_HOME_USER", "prob_" ^ prover)
@@ -399,7 +411,7 @@
           let
             (* If slicing is disabled, we expand the last slice to fill the
                entire time available. *)
-            val actual_slices = get_slices slicing (best_slices ())
+            val actual_slices = get_slices slicing (best_slices ctxt)
             val num_actual_slices = length actual_slices
             fun monomorphize_facts facts =
               let
@@ -463,7 +475,7 @@
                 fun weights () = atp_problem_weights atp_problem
                 val core =
                   File.shell_path command ^ " " ^
-                  arguments slice slice_timeout weights ^ " " ^
+                  arguments ctxt slice slice_timeout weights ^ " " ^
                   File.shell_path prob_file
                 val command =
                   (if measure_run_time then
@@ -633,16 +645,21 @@
     UnknownError msg
 
 (* FUDGE *)
-val smt_max_slices = Unsynchronized.ref 8
-val smt_slice_fact_frac = Unsynchronized.ref 0.5
-val smt_slice_time_frac = Unsynchronized.ref 0.5
-val smt_slice_min_secs = Unsynchronized.ref 5
+val smt_max_slices =
+  Attrib.setup_config_int @{binding sledgehammer_smt_max_slices} (K 8)
+val smt_slice_fact_frac =
+  Attrib.setup_config_real @{binding sledgehammer_smt_slice_fact_frac} (K 0.5)
+val smt_slice_time_frac =
+  Attrib.setup_config_real @{binding sledgehammer_smt_slice_time_frac} (K 0.5)
+val smt_slice_min_secs =
+  Attrib.setup_config_int @{binding sledgehammer_smt_slice_min_secs} (K 5)
 
-fun smt_filter_loop name ({debug, verbose, overlord, monomorphize_limit,
-                           timeout, slicing, ...} : params)
+fun smt_filter_loop ctxt name
+                    ({debug, verbose, overlord, monomorphize_limit, timeout,
+                      slicing, ...} : params)
                     state i smt_filter =
   let
-    val max_slices = if slicing then !smt_max_slices else 1
+    val max_slices = if slicing then Config.get ctxt smt_max_slices else 1
     val repair_context =
       select_smt_solver name
       #> Config.put SMT_Config.verbose debug
@@ -652,7 +669,7 @@
                         |> (fn (path, name) => path ^ "/" ^ name))
           else
             I)
-      #> Config.put SMT_Config.infer_triggers (!smt_triggers)
+      #> Config.put SMT_Config.infer_triggers (Config.get ctxt smt_triggers)
       #> Config.put SMT_Config.monomorph_full false
       #> Config.put SMT_Config.monomorph_limit monomorphize_limit
     val state = state |> Proof.map_context repair_context
@@ -664,8 +681,9 @@
         val slice_timeout =
           if slice < max_slices then
             Int.min (ms,
-                Int.max (1000 * !smt_slice_min_secs,
-                    Real.ceil (!smt_slice_time_frac * Real.fromInt ms)))
+                Int.max (1000 * Config.get ctxt smt_slice_min_secs,
+                    Real.ceil (Config.get ctxt smt_slice_time_frac
+                               * Real.fromInt ms)))
             |> Time.fromMilliseconds
           else
             timeout
@@ -709,7 +727,8 @@
            num_facts > 0 andalso Time.> (timeout, Time.zeroTime) then
           let
             val new_num_facts =
-              Real.ceil (!smt_slice_fact_frac * Real.fromInt num_facts)
+              Real.ceil (Config.get ctxt smt_slice_fact_frac
+                         * Real.fromInt num_facts)
             val _ =
               if verbose andalso is_some outcome then
                 quote name ^ " invoked with " ^ string_of_int num_facts ^
@@ -754,12 +773,11 @@
                     : prover_problem) =
   let
     val ctxt = Proof.context_of state
-    val thy = Proof.theory_of state
     val num_facts = length facts
     val facts = facts ~~ (0 upto num_facts - 1)
-                |> map (smt_weighted_fact thy num_facts)
+                |> map (smt_weighted_fact ctxt num_facts)
     val {outcome, used_facts, run_time_in_msecs} =
-      smt_filter_loop name params state subgoal smt_filter facts
+      smt_filter_loop ctxt name params state subgoal smt_filter facts
     val (chained_lemmas, other_lemmas) = split_used_facts (map fst used_facts)
     val outcome = outcome |> Option.map failure_from_smt_failure
     val message =
diff -r 242bc53b98e5 -r 4781fcd53572 src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Mon May 02 23:01:22 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Tue May 03 00:10:22 2011 +0200
@@ -13,7 +13,7 @@
   type params = Sledgehammer_Provers.params
   type prover = Sledgehammer_Provers.prover
 
-  val auto_minimize_min_facts : int Unsynchronized.ref
+  val auto_minimize_min_facts : int Config.T
   val get_minimizing_prover : Proof.context -> bool -> string -> prover
   val run_sledgehammer :
     params -> bool -> int -> relevance_override -> (string -> minimize_command)
@@ -42,7 +42,9 @@
    else
      ":\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i)))
 
-val auto_minimize_min_facts = Unsynchronized.ref (!binary_min_facts)
+val auto_minimize_min_facts =
+  Attrib.setup_config_int @{binding sledgehammer_auto_minimize_min_facts}
+      (fn generic => Config.get_generic generic binary_min_facts)
 
 fun get_minimizing_prover ctxt auto name
         (params as {debug, verbose, explicit_apply, ...}) minimize_command
@@ -54,7 +56,8 @@
          else
            let
              val (used_facts, message) =
-               if length used_facts >= !auto_minimize_min_facts then
+               if length used_facts
+                  >= Config.get ctxt auto_minimize_min_facts then
                  minimize_facts name params (SOME explicit_apply) (not verbose)
                      subgoal subgoal_count state
                      (filter_used_facts used_facts
@@ -178,7 +181,6 @@
       val state =
         state |> Proof.map_context (Config.put SMT_Config.verbose debug)
       val ctxt = Proof.context_of state
-      val thy = Proof_Context.theory_of ctxt
       val {facts = chained_ths, goal, ...} = Proof.goal state
       val (_, hyp_ts, concl_t) = strip_subgoal goal i
       val _ = () |> not blocking ? kill_provers
@@ -250,7 +252,7 @@
         else
           let
             val facts = get_facts "SMT solver" smt_relevance_fudge smts
-            val weight = SMT_Weighted_Fact oo weight_smt_fact thy
+            val weight = SMT_Weighted_Fact oo weight_smt_fact ctxt
             fun smt_filter facts =
               (if debug then curry (op o) SOME
                else TimeLimit.timeLimit timeout o try)
diff -r 242bc53b98e5 -r 4781fcd53572 src/HOL/ex/TPTP_Export.thy
--- a/src/HOL/ex/TPTP_Export.thy	Mon May 02 23:01:22 2011 +0200
+++ b/src/HOL/ex/TPTP_Export.thy	Tue May 03 00:10:22 2011 +0200
@@ -3,35 +3,36 @@
 uses "tptp_export.ML"
 begin
 
-ML {*
-val readable_names = !Sledgehammer_ATP_Translate.readable_names;
-Sledgehammer_ATP_Translate.readable_names := false
-*}
+declare [[sledgehammer_atp_readable_names = false]]
 
 ML {*
-val thy = @{theory Complex_Main}
+val do_it = false; (* switch to true to generate files *)
+val thy = @{theory Complex_Main};
 val ctxt = @{context}
 *}
 
-(*
 ML {*
-TPTP_Export.generate_tptp_inference_file_for_theory ctxt thy true
-    "/tmp/infs_full_types.tptp"
+if do_it then
+  TPTP_Export.generate_tptp_inference_file_for_theory ctxt thy true
+      "/tmp/infs_full_types.tptp"
+else
+  ()
 *}
 
 ML {*
-TPTP_Export.generate_tptp_inference_file_for_theory ctxt thy false
-    "/tmp/infs_partial_types.tptp"
+if do_it then
+  TPTP_Export.generate_tptp_inference_file_for_theory ctxt thy false
+      "/tmp/infs_partial_types.tptp"
+else
+  ()
 *}
 
 ML {*
-TPTP_Export.generate_tptp_graph_file_for_theory ctxt thy
-    "/tmp/graph.out"
-*}
-*)
-
-ML {*
-Sledgehammer_ATP_Translate.readable_names := readable_names
+if do_it then
+  TPTP_Export.generate_tptp_graph_file_for_theory ctxt thy
+      "/tmp/graph.out"
+else
+  ()
 *}
 
 end