diff -r 890b68e1e8b6 -r f9d1442c70f3 src/Pure/General/binding.ML
--- a/src/Pure/General/binding.ML	Mon Mar 30 22:34:59 2015 +0200
+++ b/src/Pure/General/binding.ML	Tue Mar 31 00:11:54 2015 +0200
@@ -10,7 +10,7 @@
 signature BINDING =
 sig
   eqtype binding
-  val dest: binding -> {private: bool, conceal: bool, path: (string * bool) list, name: bstring}
+  val dest: binding -> {private: bool, concealed: bool, path: (string * bool) list, name: bstring}
   val path_of: binding -> (string * bool) list
   val make: bstring * Position.T -> binding
   val pos_of: binding -> Position.T
@@ -30,7 +30,7 @@
   val map_prefix: ((string * bool) list -> (string * bool) list) -> binding -> binding
   val prefix: bool -> string -> binding -> binding
   val private: binding -> binding
-  val conceal: binding -> binding
+  val concealed: binding -> binding
   val pretty: binding -> Pretty.T
   val print: binding -> string
   val pp: binding -> Pretty.T
@@ -47,21 +47,21 @@
 
 datatype binding = Binding of
  {private: bool,                    (*entry is strictly private -- no name space accesses*)
-  conceal: bool,                    (*entry is for foundational purposes -- please ignore*)
+  concealed: bool,                  (*entry is for foundational purposes -- please ignore*)
   prefix: (string * bool) list,     (*system prefix*)
   qualifier: (string * bool) list,  (*user qualifier*)
   name: bstring,                    (*base name*)
   pos: Position.T};                 (*source position*)
 
-fun make_binding (private, conceal, prefix, qualifier, name, pos) =
-  Binding {private = private, conceal = conceal, prefix = prefix,
+fun make_binding (private, concealed, prefix, qualifier, name, pos) =
+  Binding {private = private, concealed = concealed, prefix = prefix,
     qualifier = qualifier, name = name, pos = pos};
 
-fun map_binding f (Binding {private, conceal, prefix, qualifier, name, pos}) =
-  make_binding (f (private, conceal, prefix, qualifier, name, pos));
+fun map_binding f (Binding {private, concealed, prefix, qualifier, name, pos}) =
+  make_binding (f (private, concealed, prefix, qualifier, name, pos));
 
-fun dest (Binding {private, conceal, prefix, qualifier, name, ...}) =
-  {private = private, conceal = conceal, path = prefix @ qualifier, name = name};
+fun dest (Binding {private, concealed, prefix, qualifier, name, ...}) =
+  {private = private, concealed = concealed, path = prefix @ qualifier, name = name};
 
 val path_of = #path o dest;
 
@@ -75,8 +75,8 @@
 
 fun pos_of (Binding {pos, ...}) = pos;
 fun set_pos pos =
-  map_binding (fn (private, conceal, prefix, qualifier, name, _) =>
-    (private, conceal, prefix, qualifier, name, pos));
+  map_binding (fn (private, concealed, prefix, qualifier, name, _) =>
+    (private, concealed, prefix, qualifier, name, pos));
 
 fun name name = make (name, Position.none);
 fun name_of (Binding {name, ...}) = name;
@@ -84,8 +84,8 @@
 fun eq_name (b, b') = name_of b = name_of b';
 
 fun map_name f =
-  map_binding (fn (private, conceal, prefix, qualifier, name, pos) =>
-    (private, conceal, prefix, qualifier, f name, pos));
+  map_binding (fn (private, concealed, prefix, qualifier, name, pos) =>
+    (private, concealed, prefix, qualifier, f name, pos));
 
 val prefix_name = map_name o prefix;
 val suffix_name = map_name o suffix;
@@ -98,13 +98,13 @@
 
 fun qualify _ "" = I
   | qualify mandatory qual =
-      map_binding (fn (private, conceal, prefix, qualifier, name, pos) =>
-        (private, conceal, prefix, (qual, mandatory) :: qualifier, name, pos));
+      map_binding (fn (private, concealed, prefix, qualifier, name, pos) =>
+        (private, concealed, prefix, (qual, mandatory) :: qualifier, name, pos));
 
 fun qualified mandatory name' =
-  map_binding (fn (private, conceal, prefix, qualifier, name, pos) =>
+  map_binding (fn (private, concealed, prefix, qualifier, name, pos) =>
     let val qualifier' = if name = "" then qualifier else qualifier @ [(name, mandatory)]
-    in (private, conceal, prefix, qualifier', name', pos) end);
+    in (private, concealed, prefix, qualifier', name', pos) end);
 
 fun qualified_name "" = empty
   | qualified_name s =
@@ -117,8 +117,8 @@
 fun prefix_of (Binding {prefix, ...}) = prefix;
 
 fun map_prefix f =
-  map_binding (fn (private, conceal, prefix, qualifier, name, pos) =>
-    (private, conceal, f prefix, qualifier, name, pos));
+  map_binding (fn (private, concealed, prefix, qualifier, name, pos) =>
+    (private, concealed, f prefix, qualifier, name, pos));
 
 fun prefix _ "" = I
   | prefix mandatory prfx = map_prefix (cons (prfx, mandatory));
@@ -127,10 +127,10 @@
 (* visibility flags *)
 
 val private =
-  map_binding (fn (_, conceal, prefix, qualifier, name, pos) =>
-    (true, conceal, prefix, qualifier, name, pos));
+  map_binding (fn (_, concealed, prefix, qualifier, name, pos) =>
+    (true, concealed, prefix, qualifier, name, pos));
 
-val conceal =
+val concealed =
   map_binding (fn (private, _, prefix, qualifier, name, pos) =>
     (private, true, prefix, qualifier, name, pos));