src/Pure/Syntax/ast.ML

   | unfold_ast_p _ y = ([], y);
 
 
 (** normalization of asts **)
 
-(* tracing options *)
-
-val trace_ast = ref false;
-val stat_ast = ref false;
-
-
 (* match *)
 
 fun match ast pat =
   let
     exception NO_MATCH;

       | rewrite (ast as Appl (Constant a :: _)) = try ast a
       | rewrite (ast as Appl (Variable a :: _)) = try ast a
       | rewrite ast = try_headless_rules ast;
 
     fun rewrote old_ast new_ast =
-      if trace then
-        writeln ("rewrote: " ^ str_of_ast old_ast ^ "  ->  " ^ str_of_ast new_ast)
-      else ();
+      conditional trace (fn () =>
+        tracing ("rewrote: " ^ str_of_ast old_ast ^ "  ->  " ^ str_of_ast new_ast));
 
     fun norm_root ast =
       (case rewrite ast of
         Some new_ast => (rewrote ast new_ast; norm_root new_ast)
       | None => ast);

         inc passes;
         if old_changes = ! changes then new_ast else normal new_ast
       end;
 
 
-    val _ = if trace then writeln ("pre: " ^ str_of_ast pre_ast) else ();
+    val _ = conditional trace (fn () => tracing ("pre: " ^ str_of_ast pre_ast));
 
     val post_ast = normal pre_ast;
   in
-    if trace orelse stat then
-      writeln ("post: " ^ str_of_ast post_ast ^ "\nnormalize: " ^
+    conditional (trace orelse stat) (fn () =>
+      tracing ("post: " ^ str_of_ast post_ast ^ "\nnormalize: " ^
         string_of_int (! passes) ^ " passes, " ^
         string_of_int (! changes) ^ " changes, " ^
-        string_of_int (! failed_matches) ^ " matches failed")
-    else ();
+        string_of_int (! failed_matches) ^ " matches failed"));
     post_ast
   end;
 
 
 (* normalize_ast *)
+
+val trace_ast = ref false;
+val stat_ast = ref false;
 
 fun normalize_ast get_rules ast =
   normalize (! trace_ast) (! stat_ast) get_rules ast;
 
 end;