# HG changeset patch
# User griff
# Date 1288350633 -7200
# Node ID fcd0fb70994b92d54a48aa0231c2f818d6e7a565
# Parent  e2fe7e93333c86bb17215e563d84b8c306b2fd81
tracing_fn was moved to Output.Private_Hooks

diff -r e2fe7e93333c -r fcd0fb70994b ProgTutorial/First_Steps.thy
--- a/ProgTutorial/First_Steps.thy	Fri Oct 29 13:00:33 2010 +0200
+++ b/ProgTutorial/First_Steps.thy	Fri Oct 29 13:10:33 2010 +0200
@@ -174,7 +174,7 @@
 end
 
 fun redirect_tracing stream =
- Output.tracing_fn := (fn s =>
+ Output.Private_Hooks.tracing_fn := (fn s =>
     (TextIO.output (stream, (strip_specials s));
      TextIO.output (stream, "\n");
      TextIO.flushOut stream)) *}