more visibility flags on background naming;

--- 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);
 

--- a/src/Pure/Isar/local_theory.ML	Tue Mar 31 22:31:05 2015 +0200
+++ b/src/Pure/Isar/local_theory.ML	Tue Mar 31 23:42:57 2015 +0200
@@ -222,11 +222,17 @@
 fun raw_theory f = #2 o raw_theory_result (f #> pair ());
 
 fun background_theory_result f lthy =
-  lthy |> raw_theory_result (fn thy =>
-    thy
-    |> Sign.map_naming (K (background_naming_of lthy))
-    |> f
-    ||> Sign.restore_naming thy);
+  let
+    val naming =
+      background_naming_of lthy
+      |> Name_Space.transform_naming (Proof_Context.naming_of lthy);
+  in
+    lthy |> raw_theory_result (fn thy =>
+      thy
+      |> Sign.map_naming (K naming)
+      |> f
+      ||> Sign.restore_naming thy)
+  end;
 
 fun background_theory f = #2 o background_theory_result (f #> pair ());