the configuration option 'trace_simp' now uses the reference of the ProofGeneral settings menu as (dynamic) default value

--- a/src/Pure/ProofGeneral/preferences.ML	Sun Mar 28 19:34:08 2010 +0200
+++ b/src/Pure/ProofGeneral/preferences.ML	Mon Mar 29 09:06:34 2010 +0200
@@ -146,7 +146,7 @@
     "Show leading question mark of variable name"];
 
 val tracing_preferences =
- [bool_pref trace_simp_ref
+ [bool_pref trace_simp_default
     "trace-simplifier"
     "Trace simplification rules.",
   nat_pref trace_simp_depth_limit

--- a/src/Pure/meta_simplifier.ML	Sun Mar 28 19:34:08 2010 +0200
+++ b/src/Pure/meta_simplifier.ML	Mon Mar 29 09:06:34 2010 +0200
@@ -15,7 +15,7 @@
   val debug_simp_value: Config.value Config.T
   val trace_simp: bool Config.T
   val trace_simp_value: Config.value Config.T
-  val trace_simp_ref: bool Unsynchronized.ref
+  val trace_simp_default: bool Unsynchronized.ref
   val trace_simp_depth_limit: int Unsynchronized.ref
   type rrule
   val eq_rrule: rrule * rrule -> bool
@@ -277,9 +277,10 @@
 val debug_simp_value = Config.declare false "debug_simp" (K (Config.Bool false));
 val debug_simp = Config.bool debug_simp_value;
 
-val trace_simp_value = Config.declare false "trace_simp" (K (Config.Bool false));
+val trace_simp_default = Unsynchronized.ref false;
+val trace_simp_value =
+  Config.declare false "trace_simp" (fn _ => Config.Bool (!trace_simp_default));
 val trace_simp = Config.bool trace_simp_value;
-val trace_simp_ref = Unsynchronized.ref false;
 
 local
 
@@ -301,31 +302,25 @@
 fun print_term_global ss warn a thy t =
   print_term ss warn (K a) t (ProofContext.init thy);
 
-fun if_enabled (Simpset ({context, ...}, _)) b flag f =
+fun if_enabled (Simpset ({context, ...}, _)) flag f =
   (case context of
-    SOME ctxt => if b orelse Config.get ctxt flag then f ctxt else ()
+    SOME ctxt => if Config.get ctxt flag then f ctxt else ()
   | NONE => ())
 
-fun debug warn a ss =
-  if_enabled ss false debug_simp (fn _ => prnt ss warn (a ()));
-fun trace warn a ss =
-  if_enabled ss (!trace_simp_ref) trace_simp (fn _ => prnt ss warn (a ()));
+fun debug warn a ss = if_enabled ss debug_simp (fn _ => prnt ss warn (a ()));
+fun trace warn a ss = if_enabled ss trace_simp (fn _ => prnt ss warn (a ()));
 
-fun debug_term warn a ss t =
-  if_enabled ss false debug_simp (print_term ss warn a t);
-fun trace_term warn a ss t =
-  if_enabled ss (!trace_simp_ref) trace_simp (print_term ss warn a t);
+fun debug_term warn a ss t = if_enabled ss debug_simp (print_term ss warn a t);
+fun trace_term warn a ss t = if_enabled ss trace_simp (print_term ss warn a t);
 
 fun trace_cterm warn a ss ct =
-  if_enabled ss (!trace_simp_ref) trace_simp
-    (print_term ss warn a (Thm.term_of ct));
+  if_enabled ss trace_simp (print_term ss warn a (Thm.term_of ct));
 
 fun trace_thm a ss th =
-  if_enabled ss (!trace_simp_ref) trace_simp
-    (print_term ss false a (Thm.full_prop_of th));
+  if_enabled ss trace_simp (print_term ss false a (Thm.full_prop_of th));
 
 fun trace_named_thm a ss (th, name) =
-  if_enabled ss (!trace_simp_ref) trace_simp (print_term ss false
+  if_enabled ss trace_simp (print_term ss false
     (fn () => if name = "" then a () else a () ^ " " ^ quote name ^ ":")
     (Thm.full_prop_of th));