| changeset 59939 | 7d46aa03696e |
| parent 59923 | b21c82422d65 |
| child 59990 | a81dc82ecba3 |
--- a/src/Pure/sign.ML Mon Apr 06 17:28:07 2015 +0200 +++ b/src/Pure/sign.ML Mon Apr 06 22:11:01 2015 +0200 @@ -525,6 +525,8 @@ val private_scope = map_naming o Name_Space.private_scope; val private = map_naming o Name_Space.private; +val restricted_scope = map_naming o Name_Space.restricted_scope; +val restricted = map_naming o Name_Space.restricted; val concealed = map_naming Name_Space.concealed;