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