diff -r 7e33ba6190de -r 07be4fccd329 ProgTutorial/Base.thy
--- a/ProgTutorial/Base.thy	Wed Jul 28 11:47:21 2010 +0100
+++ b/ProgTutorial/Base.thy	Wed Jul 28 20:52:42 2010 +0100
@@ -8,12 +8,6 @@
 notation (latex output)
   Cons ("_ # _" [66,65] 65)
 
-(* 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; *)