ProgTutorial/First_Steps.thy
changeset 455 fcd0fb70994b
parent 451 fc074e669f9f
child 458 242e81f4d461
--- 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)) *}