# HG changeset patch
# User wenzelm
# Date 959695347 -7200
# Node ID da290d99d8b22d46d7039ff52480ae9c3ef3d63f
# Parent  5a5bbb6b668849c6e44b80d1c193378889caca76
renamed trace/stat_norm_ast to trace/stat_ast;

diff -r 5a5bbb6b6688 -r da290d99d8b2 src/Pure/Syntax/ast.ML
--- a/src/Pure/Syntax/ast.ML	Tue May 30 16:01:29 2000 +0200
+++ b/src/Pure/Syntax/ast.ML	Tue May 30 16:02:27 2000 +0200
@@ -22,8 +22,8 @@
   val pretty_ast: ast -> Pretty.T
   val pretty_rule: ast * ast -> Pretty.T
   val pprint_ast: ast -> pprint_args -> unit
-  val trace_norm_ast: bool ref
-  val stat_norm_ast: bool ref
+  val trace_ast: bool ref
+  val stat_ast: bool ref
   end;
 
 signature AST =
@@ -161,8 +161,8 @@
 
 (* tracing options *)
 
-val trace_norm_ast = ref false;
-val stat_norm_ast = ref false;
+val trace_ast = ref false;
+val stat_ast = ref false;
 
 
 (* match *)
@@ -275,7 +275,7 @@
 (* normalize_ast *)
 
 fun normalize_ast get_rules ast =
-  normalize (! trace_norm_ast) (! stat_norm_ast) get_rules ast;
+  normalize (! trace_ast) (! stat_ast) get_rules ast;
 
 end;