src/Pure/General/name_space.ML
changeset 59887 43dc3c660f41
parent 59886 e0dc738eb08c
child 59888 27e4d0ab0948
--- a/src/Pure/General/name_space.ML	Tue Mar 31 22:31:05 2015 +0200
+++ b/src/Pure/General/name_space.ML	Tue Mar 31 23:42:57 2015 +0200
@@ -48,6 +48,7 @@
   val qualified_path: bool -> binding -> naming -> naming
   val global_naming: naming
   val local_naming: naming
+  val transform_naming: naming -> naming -> naming
   val transform_binding: naming -> binding -> binding
   val full_name: naming -> binding -> string
   val base_name: binding -> string
@@ -342,12 +343,19 @@
 val local_naming = global_naming |> add_path Long_Name.localN;
 
 
-(* full name *)
+(* visibility flags *)
+
+fun transform_naming (Naming {private = private', concealed = concealed', ...}) =
+  fold private (the_list private') #>
+  concealed' ? concealed;
 
 fun transform_binding (Naming {private, concealed, ...}) =
   Binding.private_default private #>
   concealed ? Binding.concealed;
 
+
+(* full name *)
+
 fun name_spec naming binding =
   Binding.name_spec (get_scopes naming) (get_path naming) (transform_binding naming binding);