# HG changeset patch
# User wenzelm
# Date 1307699272 -7200
# Node ID f18cf88453d639de79c88b27b0bf0e01788c7876
# Parent  911cb8242dfe531dca4fc09ba33e2a7880242b2e
tuned name (cf. blast_stats);

diff -r 911cb8242dfe -r f18cf88453d6 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Fri Jun 10 11:39:23 2011 +0200
+++ b/src/Pure/Isar/attrib.ML	Fri Jun 10 11:47:52 2011 +0200
@@ -420,7 +420,7 @@
 
 val _ = Context.>> (Context.map_theory
  (register_config Ast.trace_raw #>
-  register_config Ast.stat_raw #>
+  register_config Ast.stats_raw #>
   register_config Syntax.positions_raw #>
   register_config Printer.show_brackets_raw #>
   register_config Printer.show_sorts_raw #>
diff -r 911cb8242dfe -r f18cf88453d6 src/Pure/Syntax/ast.ML
--- a/src/Pure/Syntax/ast.ML	Fri Jun 10 11:39:23 2011 +0200
+++ b/src/Pure/Syntax/ast.ML	Fri Jun 10 11:47:52 2011 +0200
@@ -23,8 +23,8 @@
   val unfold_ast_p: string -> ast -> ast list * ast
   val trace_raw: Config.raw
   val trace: bool Config.T
-  val stat_raw: Config.raw
-  val stat: bool Config.T
+  val stats_raw: Config.raw
+  val stats: bool Config.T
   val normalize: Proof.context -> (string -> (ast * ast) list) -> ast -> ast
 end;
 
@@ -167,8 +167,8 @@
 val trace_raw = Config.declare "syntax_ast_trace" (fn _ => Config.Bool false);
 val trace = Config.bool trace_raw;
 
-val stat_raw = Config.declare "syntax_ast_stat" (fn _ => Config.Bool false);
-val stat = Config.bool stat_raw;
+val stats_raw = Config.declare "syntax_ast_stats" (fn _ => Config.Bool false);
+val stats = Config.bool stats_raw;
 
 fun message head body =
   Pretty.string_of (Pretty.block [Pretty.str head, Pretty.brk 1, body]);
@@ -177,7 +177,7 @@
 fun normalize ctxt get_rules pre_ast =
   let
     val trace = Config.get ctxt trace;
-    val stat = Config.get ctxt stat;
+    val stats = Config.get ctxt stats;
 
     val passes = Unsynchronized.ref 0;
     val failed_matches = Unsynchronized.ref 0;
@@ -239,7 +239,7 @@
     val _ = if trace then tracing (message "pre:" (pretty_ast pre_ast)) else ();
     val post_ast = normal pre_ast;
     val _ =
-      if trace orelse stat then
+      if trace orelse stats then
         tracing (message "post:" (pretty_ast post_ast) ^ "\nnormalize: " ^
           string_of_int (! passes) ^ " passes, " ^
           string_of_int (! changes) ^ " changes, " ^