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