--- a/ProgTutorial/Base.thy	Mon Apr 26 05:20:01 2010 +0200
+++ b/ProgTutorial/Base.thy	Mon May 17 17:27:21 2010 +0100
@@ -28,7 +28,7 @@
 ML {*
 fun write_file txt thy =
 let 
-  val stream = Config.get_thy thy filename
+  val stream = Config.get_global thy filename
                |> TextIO.openAppend 
 in
   TextIO.output (stream, txt); 
@@ -73,7 +73,7 @@
   val _ = tracing ("Open File: " ^ name)
   val _ = TextIO.openOut name
 in 
-  Config.put_thy filename name thy
+  Config.put_global filename name thy
 end
 *}