--- a/ProgTutorial/Base.thy	Mon Apr 13 08:30:48 2009 +0000
+++ b/ProgTutorial/Base.thy	Wed Apr 15 13:11:08 2009 +0000
@@ -36,10 +36,5 @@
     (OuterParse.ML_source >> IsarCmd.ml_diag true);
 
 *}
-(*
-ML {*
-  fun warning str = str
-  fun tracing str = str
-*}
-*)
-end
+
+end
\ No newline at end of file