tracing_fn was moved to Output.Private_Hooks
authorgriff
Fri, 29 Oct 2010 13:10:33 +0200
changeset 455 fcd0fb70994b
parent 454 e2fe7e93333c
child 456 89fccd3d5055
tracing_fn was moved to Output.Private_Hooks
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)) *}