--- a/ProgTutorial/Base.thy	Thu Aug 20 10:38:26 2009 +0200
+++ b/ProgTutorial/Base.thy	Thu Aug 20 14:19:39 2009 +0200
@@ -39,7 +39,8 @@
 ML {*
 fun open_file name =
   (tracing ("Opened File: " ^ name);
-   file_name := SOME name)
+   file_name := SOME name;
+   TextIO.openOut name; ())
 
 fun open_file_prelude name txt =
   (open_file name; write_file (txt ^ "\n"))