diff -r e79563b14b0f -r 0a25b35178c3 ProgTutorial/Essential.thy --- a/ProgTutorial/Essential.thy Mon Apr 26 05:20:01 2010 +0200 +++ b/ProgTutorial/Essential.thy Mon May 17 17:27:21 2010 +0100 @@ -1082,7 +1082,7 @@ manipulated as a configuration value: @{ML_response_fake [display,gray] - "Config.get_thy @{theory} (Unify.search_bound_value)" + "Config.get_global @{theory} (Unify.search_bound_value)" "Int 60"} If this bound is reached during unification, Isabelle prints out the