diff -r 74f0a06f751f -r d69214e47ef9 ProgTutorial/Base.thy
--- a/ProgTutorial/Base.thy	Thu Aug 20 22:30:20 2009 +0200
+++ b/ProgTutorial/Base.thy	Thu Aug 20 23:30:51 2009 +0200
@@ -5,6 +5,13 @@
   "antiquote_setup.ML"
 begin
 
+(* rebinding of writeln and tracing so that it can *)
+(* be compared in intiquotations                   *)
+ML {* 
+fun writeln s = (Output.writeln s; s)
+fun tracing s = (Output.tracing s; s)
+*}
+
 (* re-definition of various ML antiquotations    *)
 (* to have a special tag for text enclosed in ML *)