changeset 423 | 0a25b35178c3 |
parent 418 | 1d1e4cda8c54 |
child 429 | d04d1cd0e058 |
--- 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