tuned signature;

--- a/src/Pure/Isar/attrib.ML	Thu Apr 07 18:41:49 2011 +0200
+++ b/src/Pure/Isar/attrib.ML	Thu Apr 07 20:32:42 2011 +0200
@@ -398,8 +398,8 @@
 (* theory setup *)
 
 val _ = Context.>> (Context.map_theory
- (register_config Ast.ast_trace_raw #>
-  register_config Ast.ast_stat_raw #>
+ (register_config Ast.trace_raw #>
+  register_config Ast.stat_raw #>
   register_config Syntax.positions_raw #>
   register_config Syntax.show_brackets_raw #>
   register_config Syntax.show_sorts_raw #>

--- a/src/Pure/Syntax/ast.ML	Thu Apr 07 18:41:49 2011 +0200
+++ b/src/Pure/Syntax/ast.ML	Thu Apr 07 20:32:42 2011 +0200
@@ -21,10 +21,10 @@
   val fold_ast_p: string -> ast list * ast -> ast
   val unfold_ast: string -> ast -> ast list
   val unfold_ast_p: string -> ast -> ast list * ast
-  val ast_trace_raw: Config.raw
-  val ast_trace: bool Config.T
-  val ast_stat_raw: Config.raw
-  val ast_stat: bool Config.T
+  val trace_raw: Config.raw
+  val trace: bool Config.T
+  val stat_raw: Config.raw
+  val stat: bool Config.T
   val normalize: Proof.context -> (string -> (ast * ast) list) -> ast -> ast
 end;
 
@@ -164,11 +164,11 @@
 
 (* normalize *)
 
-val ast_trace_raw = Config.declare "syntax_ast_trace" (fn _ => Config.Bool false);
-val ast_trace = Config.bool ast_trace_raw;
+val trace_raw = Config.declare "syntax_ast_trace" (fn _ => Config.Bool false);
+val trace = Config.bool trace_raw;
 
-val ast_stat_raw = Config.declare "syntax_ast_stat" (fn _ => Config.Bool false);
-val ast_stat = Config.bool ast_stat_raw;
+val stat_raw = Config.declare "syntax_ast_stat" (fn _ => Config.Bool false);
+val stat = Config.bool stat_raw;
 
 fun message head body =
   Pretty.string_of (Pretty.block [Pretty.str head, Pretty.brk 1, body]);
@@ -176,8 +176,8 @@
 (*the normalizer works yoyo-like: top-down, bottom-up, top-down, ...*)
 fun normalize ctxt get_rules pre_ast =
   let
-    val trace = Config.get ctxt ast_trace;
-    val stat = Config.get ctxt ast_stat;
+    val trace = Config.get ctxt trace;
+    val stat = Config.get ctxt stat;
 
     val passes = Unsynchronized.ref 0;
     val failed_matches = Unsynchronized.ref 0;