
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)) *}




