src/Pure/sign.ML
changeset 59990 a81dc82ecba3
parent 59939 7d46aa03696e
child 61262 7bd1eb4b056e
     1.1 --- a/src/Pure/sign.ML	Thu Apr 09 15:54:09 2015 +0200
     1.2 +++ b/src/Pure/sign.ML	Thu Apr 09 20:42:32 2015 +0200
     1.3 @@ -113,6 +113,8 @@
     1.4    val local_path: theory -> theory
     1.5    val private_scope: Binding.scope -> theory -> theory
     1.6    val private: Position.T -> theory -> theory
     1.7 +  val qualified_scope: Binding.scope -> theory -> theory
     1.8 +  val qualified: Position.T -> theory -> theory
     1.9    val concealed: theory -> theory
    1.10    val hide_class: bool -> string -> theory -> theory
    1.11    val hide_type: bool -> string -> theory -> theory
    1.12 @@ -525,8 +527,8 @@
    1.13  
    1.14  val private_scope = map_naming o Name_Space.private_scope;
    1.15  val private = map_naming o Name_Space.private;
    1.16 -val restricted_scope = map_naming o Name_Space.restricted_scope;
    1.17 -val restricted = map_naming o Name_Space.restricted;
    1.18 +val qualified_scope = map_naming o Name_Space.qualified_scope;
    1.19 +val qualified = map_naming o Name_Space.qualified;
    1.20  val concealed = map_naming Name_Space.concealed;
    1.21  
    1.22