author | griff |
Fri, 29 Oct 2010 13:10:33 +0200 | |
changeset 455 | fcd0fb70994b |
parent 454 | e2fe7e93333c |
child 456 | 89fccd3d5055 |
--- 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)) *}