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

     2.1 --- a/src/Pure/meta_simplifier.ML	Sun Mar 28 19:34:08 2010 +0200
     2.2 +++ b/src/Pure/meta_simplifier.ML	Mon Mar 29 09:06:34 2010 +0200
     2.3 @@ -15,7 +15,7 @@
     2.4    val debug_simp_value: Config.value Config.T
     2.5    val trace_simp: bool Config.T
     2.6    val trace_simp_value: Config.value Config.T
     2.7 -  val trace_simp_ref: bool Unsynchronized.ref
     2.8 +  val trace_simp_default: bool Unsynchronized.ref
     2.9    val trace_simp_depth_limit: int Unsynchronized.ref
    2.10    type rrule
    2.11    val eq_rrule: rrule * rrule -> bool
    2.12 @@ -277,9 +277,10 @@
    2.13  val debug_simp_value = Config.declare false "debug_simp" (K (Config.Bool false));
    2.14  val debug_simp = Config.bool debug_simp_value;
    2.15  
    2.16 -val trace_simp_value = Config.declare false "trace_simp" (K (Config.Bool false));
    2.17 +val trace_simp_default = Unsynchronized.ref false;
    2.18 +val trace_simp_value =
    2.19 +  Config.declare false "trace_simp" (fn _ => Config.Bool (!trace_simp_default));
    2.20  val trace_simp = Config.bool trace_simp_value;
    2.21 -val trace_simp_ref = Unsynchronized.ref false;
    2.22  
    2.23  local
    2.24  
    2.25 @@ -301,31 +302,25 @@
    2.26  fun print_term_global ss warn a thy t =
    2.27    print_term ss warn (K a) t (ProofContext.init thy);
    2.28  
    2.29 -fun if_enabled (Simpset ({context, ...}, _)) b flag f =
    2.30 +fun if_enabled (Simpset ({context, ...}, _)) flag f =
    2.31    (case context of
    2.32 -    SOME ctxt => if b orelse Config.get ctxt flag then f ctxt else ()
    2.33 +    SOME ctxt => if Config.get ctxt flag then f ctxt else ()
    2.34    | NONE => ())
    2.35  
    2.36 -fun debug warn a ss =
    2.37 -  if_enabled ss false debug_simp (fn _ => prnt ss warn (a ()));
    2.38 -fun trace warn a ss =
    2.39 -  if_enabled ss (!trace_simp_ref) trace_simp (fn _ => prnt ss warn (a ()));
    2.40 +fun debug warn a ss = if_enabled ss debug_simp (fn _ => prnt ss warn (a ()));
    2.41 +fun trace warn a ss = if_enabled ss trace_simp (fn _ => prnt ss warn (a ()));
    2.42  
    2.43 -fun debug_term warn a ss t =
    2.44 -  if_enabled ss false debug_simp (print_term ss warn a t);
    2.45 -fun trace_term warn a ss t =
    2.46 -  if_enabled ss (!trace_simp_ref) trace_simp (print_term ss warn a t);
    2.47 +fun debug_term warn a ss t = if_enabled ss debug_simp (print_term ss warn a t);
    2.48 +fun trace_term warn a ss t = if_enabled ss trace_simp (print_term ss warn a t);
    2.49  
    2.50  fun trace_cterm warn a ss ct =
    2.51 -  if_enabled ss (!trace_simp_ref) trace_simp
    2.52 -    (print_term ss warn a (Thm.term_of ct));
    2.53 +  if_enabled ss trace_simp (print_term ss warn a (Thm.term_of ct));
    2.54  
    2.55  fun trace_thm a ss th =
    2.56 -  if_enabled ss (!trace_simp_ref) trace_simp
    2.57 -    (print_term ss false a (Thm.full_prop_of th));
    2.58 +  if_enabled ss trace_simp (print_term ss false a (Thm.full_prop_of th));
    2.59  
    2.60  fun trace_named_thm a ss (th, name) =
    2.61 -  if_enabled ss (!trace_simp_ref) trace_simp (print_term ss false
    2.62 +  if_enabled ss trace_simp (print_term ss false
    2.63      (fn () => if name = "" then a () else a () ^ " " ^ quote name ^ ":")
    2.64      (Thm.full_prop_of th));
    2.65