
diff -r e79563b14b0f -r 0a25b35178c3 ProgTutorial/FirstSteps.thy
--- a/ProgTutorial/FirstSteps.thy	Mon Apr 26 05:20:01 2010 +0200
+++ b/ProgTutorial/FirstSteps.thy	Mon May 17 17:27:21 2010 +0100
@@ -1378,15 +1378,15 @@
   "Config.get @{context} bval" 
   "true"}
 
-  or directly from a theory using the function @{ML_ind get_thy in Config}
+  or directly from a theory using the function @{ML_ind get_global in Config}
 
   @{ML_response [display,gray] 
-  "Config.get_thy @{theory} bval" 
+  "Config.get_global @{theory} bval" 
   "true"}
 
   It is also possible to manipulate the configuration values
   from the ML-level with the functions @{ML_ind put in Config}
-  and @{ML_ind put_thy in Config}. For example
+  and @{ML_ind put_global in Config}. For example
 
   @{ML_response [display,gray]
   "let




