diff -r 890b68e1e8b6 -r f9d1442c70f3 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Mon Mar 30 22:34:59 2015 +0200
+++ b/src/Pure/General/name_space.ML	Tue Mar 31 00:11:54 2015 +0200
@@ -34,7 +34,7 @@
   val merge: T * T -> T
   type naming
   val private: naming -> naming
-  val conceal: naming -> naming
+  val concealed: naming -> naming
   val get_group: naming -> serial option
   val set_group: serial option -> naming -> naming
   val set_theory_name: string -> naming -> naming
@@ -285,36 +285,36 @@
 
 datatype naming = Naming of
  {private: bool,
-  conceal: bool,
+  concealed: bool,
   group: serial option,
   theory_name: string,
   path: (string * bool) list};
 
-fun make_naming (private, conceal, group, theory_name, path) =
-  Naming {private = private, conceal = conceal, group = group,
+fun make_naming (private, concealed, group, theory_name, path) =
+  Naming {private = private, concealed = concealed, group = group,
     theory_name = theory_name, path = path};
 
-fun map_naming f (Naming {private, conceal, group, theory_name, path}) =
-  make_naming (f (private, conceal, group, theory_name, path));
+fun map_naming f (Naming {private, concealed, group, theory_name, path}) =
+  make_naming (f (private, concealed, group, theory_name, path));
 
-fun map_path f = map_naming (fn (private, conceal, group, theory_name, path) =>
-  (private, conceal, group, theory_name, f path));
+fun map_path f = map_naming (fn (private, concealed, group, theory_name, path) =>
+  (private, concealed, group, theory_name, f path));
 
 
-val private = map_naming (fn (_, conceal, group, theory_name, path) =>
-  (true, conceal, group, theory_name, path));
+val private = map_naming (fn (_, concealed, group, theory_name, path) =>
+  (true, concealed, group, theory_name, path));
 
-val conceal = map_naming (fn (private, _, group, theory_name, path) =>
+val concealed = map_naming (fn (private, _, group, theory_name, path) =>
   (private, true, group, theory_name, path));
 
-fun set_theory_name theory_name = map_naming (fn (private, conceal, group, _, path) =>
-  (private, conceal, group, theory_name, path));
+fun set_theory_name theory_name = map_naming (fn (private, concealed, group, _, path) =>
+  (private, concealed, group, theory_name, path));
 
 
 fun get_group (Naming {group, ...}) = group;
 
-fun set_group group = map_naming (fn (private, conceal, _, theory_name, path) =>
-  (private, conceal, group, theory_name, path));
+fun set_group group = map_naming (fn (private, concealed, _, theory_name, path) =>
+  (private, concealed, group, theory_name, path));
 
 fun new_group naming = set_group (SOME (serial ())) naming;
 val reset_group = set_group NONE;
@@ -335,16 +335,16 @@
 
 fun err_bad binding = error (Binding.bad binding);
 
-fun transform_binding (Naming {private, conceal, ...}) =
+fun transform_binding (Naming {private, concealed, ...}) =
   private ? Binding.private #>
-  conceal ? Binding.conceal;
+  concealed ? Binding.concealed;
 
 val bad_specs = ["", "??", "__"];
 
 fun name_spec (naming as Naming {path = path1, ...}) raw_binding =
   let
     val binding = transform_binding naming raw_binding;
-    val {private, conceal, path = path2, name} = Binding.dest binding;
+    val {private, concealed, path = path2, name} = Binding.dest binding;
     val _ = Long_Name.is_qualified name andalso err_bad binding;
 
     val spec1 = maps (fn (a, b) => map (rpair b) (Long_Name.explode a)) (path1 @ path2);
@@ -353,7 +353,7 @@
     val _ =
       exists (fn (a, _) => member (op =) bad_specs a orelse exists_string (fn s => s = "\"") a) spec
       andalso err_bad binding;
-  in {private = private, conceal = conceal, spec = if null spec2 then [] else spec} end;
+  in {private = private, concealed = concealed, spec = if null spec2 then [] else spec} end;
 
 fun full_name naming =
   name_spec naming #> #spec #> map #1 #> Long_Name.implode;
@@ -442,7 +442,7 @@
   let
     val naming = naming_of context;
     val Naming {group, theory_name, ...} = naming;
-    val {conceal, spec, ...} = name_spec naming binding;
+    val {concealed, spec, ...} = name_spec naming binding;
     val (accs, accs') = accesses naming binding;
 
     val name = Long_Name.implode (map fst spec);
@@ -450,7 +450,7 @@
 
     val (proper_pos, pos) = Position.default (Binding.pos_of binding);
     val entry =
-     {concealed = conceal,
+     {concealed = concealed,
       group = group,
       theory_name = theory_name,
       pos = pos,