# HG changeset patch
# User wenzelm
# Date 1291302262 -3600
# Node ID 7695e4de4d8658cc45b46a0b6bf5106e1d2f5e81
# Parent  9e1136e8bb1f8f0ac4e4cbf1fe9afea3aa9dc530
renamed trace_simp to simp_trace, and debug_simp to simp_debug;

diff -r 9e1136e8bb1f -r 7695e4de4d86 NEWS
--- a/NEWS	Thu Dec 02 15:37:32 2010 +0100
+++ b/NEWS	Thu Dec 02 16:04:22 2010 +0100
@@ -60,6 +60,12 @@
 Note that corresponding "..._default" references in ML may be only
 changed globally at the ROOT session setup, but *not* within a theory.
 
+* More systematic naming of some configuration options.
+  INCOMPATIBILTY.
+
+  trace_simp  ~>  simp_trace
+  debug_simp  ~>  simp_debug
+
 
 *** Pure ***
 
diff -r 9e1136e8bb1f -r 7695e4de4d86 doc-src/TutorialI/Misc/simp.thy
--- a/doc-src/TutorialI/Misc/simp.thy	Thu Dec 02 15:37:32 2010 +0100
+++ b/doc-src/TutorialI/Misc/simp.thy	Thu Dec 02 16:04:22 2010 +0100
@@ -422,7 +422,7 @@
 
 (*<*)lemma "x=x"
 (*>*)
-using [[trace_simp=true]]
+using [[simp_trace=true]]
 apply simp
 (*<*)oops(*>*)
 
diff -r 9e1136e8bb1f -r 7695e4de4d86 doc-src/TutorialI/Recdef/Nested2.thy
--- a/doc-src/TutorialI/Recdef/Nested2.thy	Thu Dec 02 15:37:32 2010 +0100
+++ b/doc-src/TutorialI/Recdef/Nested2.thy	Thu Dec 02 16:04:22 2010 +0100
@@ -30,7 +30,7 @@
 text{*\noindent
 If the proof of the induction step mystifies you, we recommend that you go through
 the chain of simplification steps in detail; you will probably need the help of
-@{text"trace_simp"}. Theorem @{thm[source]map_cong} is discussed below.
+@{text"simp_trace"}. Theorem @{thm[source]map_cong} is discussed below.
 %\begin{quote}
 %{term[display]"trev(trev(App f ts))"}\\
 %{term[display]"App f (rev(map trev (rev(map trev ts))))"}\\
diff -r 9e1136e8bb1f -r 7695e4de4d86 src/HOL/Tools/nat_numeral_simprocs.ML
--- a/src/HOL/Tools/nat_numeral_simprocs.ML	Thu Dec 02 15:37:32 2010 +0100
+++ b/src/HOL/Tools/nat_numeral_simprocs.ML	Thu Dec 02 16:04:22 2010 +0100
@@ -446,7 +446,7 @@
 (*examples:
 print_depth 22;
 set timing;
-set trace_simp;
+set simp_trace;
 fun test s = (Goal s; by (Simp_tac 1));
 
 (*cancel_numerals*)
diff -r 9e1136e8bb1f -r 7695e4de4d86 src/HOL/Tools/numeral_simprocs.ML
--- a/src/HOL/Tools/numeral_simprocs.ML	Thu Dec 02 15:37:32 2010 +0100
+++ b/src/HOL/Tools/numeral_simprocs.ML	Thu Dec 02 16:04:22 2010 +0100
@@ -764,7 +764,7 @@
 (*examples:
 print_depth 22;
 set timing;
-set trace_simp;
+set simp_trace;
 fun test s = (Goal s, by (Simp_tac 1));
 
 test "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = (uu::int)";
@@ -803,7 +803,7 @@
 (*examples:
 print_depth 22;
 set timing;
-set trace_simp;
+set simp_trace;
 fun test s = (Goal s; by (Simp_tac 1));
 
 test "9*x = 12 * (y::int)";
@@ -873,7 +873,7 @@
 (*examples:
 print_depth 22;
 set timing;
-set trace_simp;
+set simp_trace;
 fun test s = (Goal s; by (Asm_simp_tac 1));
 
 test "x*k = k*(y::int)";
@@ -890,7 +890,7 @@
 (*And the same examples for fields such as rat or real:
 print_depth 22;
 set timing;
-set trace_simp;
+set simp_trace;
 fun test s = (Goal s; by (Asm_simp_tac 1));
 
 test "x*k = k*(y::rat)";
diff -r 9e1136e8bb1f -r 7695e4de4d86 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Thu Dec 02 15:37:32 2010 +0100
+++ b/src/Pure/Isar/attrib.ML	Thu Dec 02 16:04:22 2010 +0100
@@ -415,7 +415,7 @@
   register_config Unify.trace_simp_raw #>
   register_config Unify.trace_types_raw #>
   register_config MetaSimplifier.simp_depth_limit_raw #>
-  register_config MetaSimplifier.debug_simp_raw #>
-  register_config MetaSimplifier.trace_simp_raw));
+  register_config MetaSimplifier.simp_debug_raw #>
+  register_config MetaSimplifier.simp_trace_raw));
 
 end;
diff -r 9e1136e8bb1f -r 7695e4de4d86 src/Pure/ProofGeneral/preferences.ML
--- a/src/Pure/ProofGeneral/preferences.ML	Thu Dec 02 15:37:32 2010 +0100
+++ b/src/Pure/ProofGeneral/preferences.ML	Thu Dec 02 16:04:22 2010 +0100
@@ -147,10 +147,10 @@
     "Show leading question mark of variable name"];
 
 val tracing_preferences =
- [bool_pref trace_simp_default
+ [bool_pref simp_trace_default
     "trace-simplifier"
     "Trace simplification rules.",
-  nat_pref trace_simp_depth_limit
+  nat_pref simp_trace_depth_limit
     "trace-simplifier-depth"
     "Trace simplifier depth limit.",
   bool_pref trace_rules
diff -r 9e1136e8bb1f -r 7695e4de4d86 src/Pure/meta_simplifier.ML
--- a/src/Pure/meta_simplifier.ML	Thu Dec 02 15:37:32 2010 +0100
+++ b/src/Pure/meta_simplifier.ML	Thu Dec 02 16:04:22 2010 +0100
@@ -11,12 +11,12 @@
 
 signature BASIC_META_SIMPLIFIER =
 sig
-  val debug_simp: bool Config.T
-  val debug_simp_raw: Config.raw
-  val trace_simp: bool Config.T
-  val trace_simp_raw: Config.raw
-  val trace_simp_default: bool Unsynchronized.ref
-  val trace_simp_depth_limit: int Unsynchronized.ref
+  val simp_debug: bool Config.T
+  val simp_debug_raw: Config.raw
+  val simp_trace: bool Config.T
+  val simp_trace_raw: Config.raw
+  val simp_trace_default: bool Unsynchronized.ref
+  val simp_trace_depth_limit: int Unsynchronized.ref
   type rrule
   val eq_rrule: rrule * rrule -> bool
   type simpset
@@ -253,18 +253,18 @@
 val simp_depth_limit_raw = Config.declare "simp_depth_limit" (K (Config.Int 100));
 val simp_depth_limit = Config.int simp_depth_limit_raw;
 
-val trace_simp_depth_limit = Unsynchronized.ref 1;
+val simp_trace_depth_limit = Unsynchronized.ref 1;
 
 fun trace_depth (Simpset ({depth = (depth, exceeded), ...}, _)) msg =
-  if depth > ! trace_simp_depth_limit then
-    if ! exceeded then () else (tracing "trace_simp_depth_limit exceeded!"; exceeded := true)
+  if depth > ! simp_trace_depth_limit then
+    if ! exceeded then () else (tracing "simp_trace_depth_limit exceeded!"; exceeded := true)
   else
     (tracing (enclose "[" "]" (string_of_int depth) ^ msg); exceeded := false);
 
 val inc_simp_depth = map_simpset1 (fn (rules, prems, bounds, (depth, exceeded), context) =>
   (rules, prems, bounds,
     (depth + 1,
-      if depth = ! trace_simp_depth_limit then Unsynchronized.ref false else exceeded), context));
+      if depth = ! simp_trace_depth_limit then Unsynchronized.ref false else exceeded), context));
 
 fun simp_depth (Simpset ({depth = (depth, _), ...}, _)) = depth;
 
@@ -273,12 +273,12 @@
 
 exception SIMPLIFIER of string * thm;
 
-val debug_simp_raw = Config.declare "debug_simp" (K (Config.Bool false));
-val debug_simp = Config.bool debug_simp_raw;
+val simp_debug_raw = Config.declare "simp_debug" (K (Config.Bool false));
+val simp_debug = Config.bool simp_debug_raw;
 
-val trace_simp_default = Unsynchronized.ref false;
-val trace_simp_raw = Config.declare "trace_simp" (fn _ => Config.Bool (! trace_simp_default));
-val trace_simp = Config.bool trace_simp_raw;
+val simp_trace_default = Unsynchronized.ref false;
+val simp_trace_raw = Config.declare "simp_trace" (fn _ => Config.Bool (! simp_trace_default));
+val simp_trace = Config.bool simp_trace_raw;
 
 fun if_enabled (Simpset ({context, ...}, _)) flag f =
   (case context of
@@ -303,27 +303,27 @@
 
 fun print_term ss warn a t ctxt = prnt ss warn (a () ^ "\n" ^
   Syntax.string_of_term ctxt
-    (if Config.get ctxt debug_simp then t else show_bounds ss t));
+    (if Config.get ctxt simp_debug then t else show_bounds ss t));
 
 in
 
 fun print_term_global ss warn a thy t =
   print_term ss warn (K a) t (ProofContext.init_global thy);
 
-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 warn a ss = if_enabled ss simp_debug (fn _ => prnt ss warn (a ()));
+fun trace warn a ss = if_enabled ss simp_trace (fn _ => prnt ss warn (a ()));
 
-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 debug_term warn a ss t = if_enabled ss simp_debug (print_term ss warn a t);
+fun trace_term warn a ss t = if_enabled ss simp_trace (print_term ss warn a t);
 
 fun trace_cterm warn a ss ct =
-  if_enabled ss trace_simp (print_term ss warn a (Thm.term_of ct));
+  if_enabled ss simp_trace (print_term ss warn a (Thm.term_of ct));
 
 fun trace_thm a ss th =
-  if_enabled ss trace_simp (print_term ss false a (Thm.full_prop_of th));
+  if_enabled ss simp_trace (print_term ss false a (Thm.full_prop_of th));
 
 fun trace_named_thm a ss (th, name) =
-  if_enabled ss trace_simp (print_term ss false
+  if_enabled ss simp_trace (print_term ss false
     (fn () => if name = "" then a () else a () ^ " " ^ quote name ^ ":")
     (Thm.full_prop_of th));
 
diff -r 9e1136e8bb1f -r 7695e4de4d86 src/ZF/arith_data.ML
--- a/src/ZF/arith_data.ML	Thu Dec 02 15:37:32 2010 +0100
+++ b/src/ZF/arith_data.ML	Thu Dec 02 16:04:22 2010 +0100
@@ -223,7 +223,7 @@
 (*examples:
 print_depth 22;
 set timing;
-set trace_simp;
+set simp_trace;
 fun test s = (Goal s; by (Asm_simp_tac 1));
 
 test "x #+ y = x #+ z";
diff -r 9e1136e8bb1f -r 7695e4de4d86 src/ZF/int_arith.ML
--- a/src/ZF/int_arith.ML	Thu Dec 02 15:37:32 2010 +0100
+++ b/src/ZF/int_arith.ML	Thu Dec 02 16:04:22 2010 +0100
@@ -312,7 +312,7 @@
 (*
 print_depth 22;
 set timing;
-set trace_simp;
+set simp_trace;
 fun test s = (Goal s; by (Asm_simp_tac 1));
 val sg = #sign (rep_thm (topthm()));
 val t = FOLogic.dest_Trueprop (Logic.strip_assums_concl(getgoal 1));