1.1 --- a/NEWS	Thu Dec 02 15:37:32 2010 +0100
     1.2 +++ b/NEWS	Thu Dec 02 16:04:22 2010 +0100
     1.3 @@ -60,6 +60,12 @@
     1.4  Note that corresponding "..._default" references in ML may be only
     1.5  changed globally at the ROOT session setup, but *not* within a theory.
     1.6  
     1.7 +* More systematic naming of some configuration options.
     1.8 +  INCOMPATIBILTY.
     1.9 +
    1.10 +  trace_simp  ~>  simp_trace
    1.11 +  debug_simp  ~>  simp_debug
    1.12 +
    1.13  
    1.14  *** Pure ***
    1.15  

     2.1 --- a/doc-src/TutorialI/Misc/simp.thy	Thu Dec 02 15:37:32 2010 +0100
     2.2 +++ b/doc-src/TutorialI/Misc/simp.thy	Thu Dec 02 16:04:22 2010 +0100
     2.3 @@ -422,7 +422,7 @@
     2.4  
     2.5  (*<*)lemma "x=x"
     2.6  (*>*)
     2.7 -using [[trace_simp=true]]
     2.8 +using [[simp_trace=true]]
     2.9  apply simp
    2.10  (*<*)oops(*>*)
    2.11  

     3.1 --- a/doc-src/TutorialI/Recdef/Nested2.thy	Thu Dec 02 15:37:32 2010 +0100
     3.2 +++ b/doc-src/TutorialI/Recdef/Nested2.thy	Thu Dec 02 16:04:22 2010 +0100
     3.3 @@ -30,7 +30,7 @@
     3.4  text{*\noindent
     3.5  If the proof of the induction step mystifies you, we recommend that you go through
     3.6  the chain of simplification steps in detail; you will probably need the help of
     3.7 -@{text"trace_simp"}. Theorem @{thm[source]map_cong} is discussed below.
     3.8 +@{text"simp_trace"}. Theorem @{thm[source]map_cong} is discussed below.
     3.9  %\begin{quote}
    3.10  %{term[display]"trev(trev(App f ts))"}\\
    3.11  %{term[display]"App f (rev(map trev (rev(map trev ts))))"}\\

     4.1 --- a/src/HOL/Tools/nat_numeral_simprocs.ML	Thu Dec 02 15:37:32 2010 +0100
     4.2 +++ b/src/HOL/Tools/nat_numeral_simprocs.ML	Thu Dec 02 16:04:22 2010 +0100
     4.3 @@ -446,7 +446,7 @@
     4.4  (*examples:
     4.5  print_depth 22;
     4.6  set timing;
     4.7 -set trace_simp;
     4.8 +set simp_trace;
     4.9  fun test s = (Goal s; by (Simp_tac 1));
    4.10  
    4.11  (*cancel_numerals*)

     5.1 --- a/src/HOL/Tools/numeral_simprocs.ML	Thu Dec 02 15:37:32 2010 +0100
     5.2 +++ b/src/HOL/Tools/numeral_simprocs.ML	Thu Dec 02 16:04:22 2010 +0100
     5.3 @@ -764,7 +764,7 @@
     5.4  (*examples:
     5.5  print_depth 22;
     5.6  set timing;
     5.7 -set trace_simp;
     5.8 +set simp_trace;
     5.9  fun test s = (Goal s, by (Simp_tac 1));
    5.10  
    5.11  test "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = (uu::int)";
    5.12 @@ -803,7 +803,7 @@
    5.13  (*examples:
    5.14  print_depth 22;
    5.15  set timing;
    5.16 -set trace_simp;
    5.17 +set simp_trace;
    5.18  fun test s = (Goal s; by (Simp_tac 1));
    5.19  
    5.20  test "9*x = 12 * (y::int)";
    5.21 @@ -873,7 +873,7 @@
    5.22  (*examples:
    5.23  print_depth 22;
    5.24  set timing;
    5.25 -set trace_simp;
    5.26 +set simp_trace;
    5.27  fun test s = (Goal s; by (Asm_simp_tac 1));
    5.28  
    5.29  test "x*k = k*(y::int)";
    5.30 @@ -890,7 +890,7 @@
    5.31  (*And the same examples for fields such as rat or real:
    5.32  print_depth 22;
    5.33  set timing;
    5.34 -set trace_simp;
    5.35 +set simp_trace;
    5.36  fun test s = (Goal s; by (Asm_simp_tac 1));
    5.37  
    5.38  test "x*k = k*(y::rat)";

     6.1 --- a/src/Pure/Isar/attrib.ML	Thu Dec 02 15:37:32 2010 +0100
     6.2 +++ b/src/Pure/Isar/attrib.ML	Thu Dec 02 16:04:22 2010 +0100
     6.3 @@ -415,7 +415,7 @@
     6.4    register_config Unify.trace_simp_raw #>
     6.5    register_config Unify.trace_types_raw #>
     6.6    register_config MetaSimplifier.simp_depth_limit_raw #>
     6.7 -  register_config MetaSimplifier.debug_simp_raw #>
     6.8 -  register_config MetaSimplifier.trace_simp_raw));
     6.9 +  register_config MetaSimplifier.simp_debug_raw #>
    6.10 +  register_config MetaSimplifier.simp_trace_raw));
    6.11  
    6.12  end;

     7.1 --- a/src/Pure/ProofGeneral/preferences.ML	Thu Dec 02 15:37:32 2010 +0100
     7.2 +++ b/src/Pure/ProofGeneral/preferences.ML	Thu Dec 02 16:04:22 2010 +0100
     7.3 @@ -147,10 +147,10 @@
     7.4      "Show leading question mark of variable name"];
     7.5  
     7.6  val tracing_preferences =
     7.7 - [bool_pref trace_simp_default
     7.8 + [bool_pref simp_trace_default
     7.9      "trace-simplifier"
    7.10      "Trace simplification rules.",
    7.11 -  nat_pref trace_simp_depth_limit
    7.12 +  nat_pref simp_trace_depth_limit
    7.13      "trace-simplifier-depth"
    7.14      "Trace simplifier depth limit.",
    7.15    bool_pref trace_rules

     8.1 --- a/src/Pure/meta_simplifier.ML	Thu Dec 02 15:37:32 2010 +0100
     8.2 +++ b/src/Pure/meta_simplifier.ML	Thu Dec 02 16:04:22 2010 +0100
     8.3 @@ -11,12 +11,12 @@
     8.4  
     8.5  signature BASIC_META_SIMPLIFIER =
     8.6  sig
     8.7 -  val debug_simp: bool Config.T
     8.8 -  val debug_simp_raw: Config.raw
     8.9 -  val trace_simp: bool Config.T
    8.10 -  val trace_simp_raw: Config.raw
    8.11 -  val trace_simp_default: bool Unsynchronized.ref
    8.12 -  val trace_simp_depth_limit: int Unsynchronized.ref
    8.13 +  val simp_debug: bool Config.T
    8.14 +  val simp_debug_raw: Config.raw
    8.15 +  val simp_trace: bool Config.T
    8.16 +  val simp_trace_raw: Config.raw
    8.17 +  val simp_trace_default: bool Unsynchronized.ref
    8.18 +  val simp_trace_depth_limit: int Unsynchronized.ref
    8.19    type rrule
    8.20    val eq_rrule: rrule * rrule -> bool
    8.21    type simpset
    8.22 @@ -253,18 +253,18 @@
    8.23  val simp_depth_limit_raw = Config.declare "simp_depth_limit" (K (Config.Int 100));
    8.24  val simp_depth_limit = Config.int simp_depth_limit_raw;
    8.25  
    8.26 -val trace_simp_depth_limit = Unsynchronized.ref 1;
    8.27 +val simp_trace_depth_limit = Unsynchronized.ref 1;
    8.28  
    8.29  fun trace_depth (Simpset ({depth = (depth, exceeded), ...}, _)) msg =
    8.30 -  if depth > ! trace_simp_depth_limit then
    8.31 -    if ! exceeded then () else (tracing "trace_simp_depth_limit exceeded!"; exceeded := true)
    8.32 +  if depth > ! simp_trace_depth_limit then
    8.33 +    if ! exceeded then () else (tracing "simp_trace_depth_limit exceeded!"; exceeded := true)
    8.34    else
    8.35      (tracing (enclose "[" "]" (string_of_int depth) ^ msg); exceeded := false);
    8.36  
    8.37  val inc_simp_depth = map_simpset1 (fn (rules, prems, bounds, (depth, exceeded), context) =>
    8.38    (rules, prems, bounds,
    8.39      (depth + 1,
    8.40 -      if depth = ! trace_simp_depth_limit then Unsynchronized.ref false else exceeded), context));
    8.41 +      if depth = ! simp_trace_depth_limit then Unsynchronized.ref false else exceeded), context));
    8.42  
    8.43  fun simp_depth (Simpset ({depth = (depth, _), ...}, _)) = depth;
    8.44  
    8.45 @@ -273,12 +273,12 @@
    8.46  
    8.47  exception SIMPLIFIER of string * thm;
    8.48  
    8.49 -val debug_simp_raw = Config.declare "debug_simp" (K (Config.Bool false));
    8.50 -val debug_simp = Config.bool debug_simp_raw;
    8.51 +val simp_debug_raw = Config.declare "simp_debug" (K (Config.Bool false));
    8.52 +val simp_debug = Config.bool simp_debug_raw;
    8.53  
    8.54 -val trace_simp_default = Unsynchronized.ref false;
    8.55 -val trace_simp_raw = Config.declare "trace_simp" (fn _ => Config.Bool (! trace_simp_default));
    8.56 -val trace_simp = Config.bool trace_simp_raw;
    8.57 +val simp_trace_default = Unsynchronized.ref false;
    8.58 +val simp_trace_raw = Config.declare "simp_trace" (fn _ => Config.Bool (! simp_trace_default));
    8.59 +val simp_trace = Config.bool simp_trace_raw;
    8.60  
    8.61  fun if_enabled (Simpset ({context, ...}, _)) flag f =
    8.62    (case context of
    8.63 @@ -303,27 +303,27 @@
    8.64  
    8.65  fun print_term ss warn a t ctxt = prnt ss warn (a () ^ "\n" ^
    8.66    Syntax.string_of_term ctxt
    8.67 -    (if Config.get ctxt debug_simp then t else show_bounds ss t));
    8.68 +    (if Config.get ctxt simp_debug then t else show_bounds ss t));
    8.69  
    8.70  in
    8.71  
    8.72  fun print_term_global ss warn a thy t =
    8.73    print_term ss warn (K a) t (ProofContext.init_global thy);
    8.74  
    8.75 -fun debug warn a ss = if_enabled ss debug_simp (fn _ => prnt ss warn (a ()));
    8.76 -fun trace warn a ss = if_enabled ss trace_simp (fn _ => prnt ss warn (a ()));
    8.77 +fun debug warn a ss = if_enabled ss simp_debug (fn _ => prnt ss warn (a ()));
    8.78 +fun trace warn a ss = if_enabled ss simp_trace (fn _ => prnt ss warn (a ()));
    8.79  
    8.80 -fun debug_term warn a ss t = if_enabled ss debug_simp (print_term ss warn a t);
    8.81 -fun trace_term warn a ss t = if_enabled ss trace_simp (print_term ss warn a t);
    8.82 +fun debug_term warn a ss t = if_enabled ss simp_debug (print_term ss warn a t);
    8.83 +fun trace_term warn a ss t = if_enabled ss simp_trace (print_term ss warn a t);
    8.84  
    8.85  fun trace_cterm warn a ss ct =
    8.86 -  if_enabled ss trace_simp (print_term ss warn a (Thm.term_of ct));
    8.87 +  if_enabled ss simp_trace (print_term ss warn a (Thm.term_of ct));
    8.88  
    8.89  fun trace_thm a ss th =
    8.90 -  if_enabled ss trace_simp (print_term ss false a (Thm.full_prop_of th));
    8.91 +  if_enabled ss simp_trace (print_term ss false a (Thm.full_prop_of th));
    8.92  
    8.93  fun trace_named_thm a ss (th, name) =
    8.94 -  if_enabled ss trace_simp (print_term ss false
    8.95 +  if_enabled ss simp_trace (print_term ss false
    8.96      (fn () => if name = "" then a () else a () ^ " " ^ quote name ^ ":")
    8.97      (Thm.full_prop_of th));
    8.98  

     9.1 --- a/src/ZF/arith_data.ML	Thu Dec 02 15:37:32 2010 +0100
     9.2 +++ b/src/ZF/arith_data.ML	Thu Dec 02 16:04:22 2010 +0100
     9.3 @@ -223,7 +223,7 @@
     9.4  (*examples:
     9.5  print_depth 22;
     9.6  set timing;
     9.7 -set trace_simp;
     9.8 +set simp_trace;
     9.9  fun test s = (Goal s; by (Asm_simp_tac 1));
    9.10  
    9.11  test "x #+ y = x #+ z";

    10.1 --- a/src/ZF/int_arith.ML	Thu Dec 02 15:37:32 2010 +0100
    10.2 +++ b/src/ZF/int_arith.ML	Thu Dec 02 16:04:22 2010 +0100
    10.3 @@ -312,7 +312,7 @@
    10.4  (*
    10.5  print_depth 22;
    10.6  set timing;
    10.7 -set trace_simp;
    10.8 +set simp_trace;
    10.9  fun test s = (Goal s; by (Asm_simp_tac 1));
   10.10  val sg = #sign (rep_thm (topthm()));
   10.11  val t = FOLogic.dest_Trueprop (Logic.strip_assums_concl(getgoal 1));