--- a/src/Pure/General/binding.ML Sun Jan 24 15:02:29 2016 +0100
+++ b/src/Pure/General/binding.ML Sun Jan 24 15:02:56 2016 +0100
@@ -31,7 +31,7 @@
val prefix_of: binding -> (string * bool) list
val map_prefix: ((string * bool) list -> (string * bool) list) -> binding -> binding
val prefix: bool -> string -> binding -> binding
- val restricted_default: (bool * scope) option -> binding -> binding
+ val restricted: (bool * scope) option -> binding -> binding
val concealed: binding -> binding
val pretty: binding -> Pretty.T
val print: binding -> string
@@ -135,14 +135,9 @@
(* visibility flags *)
-fun restricted strict scope =
- map_binding (fn (_, concealed, prefix, qualifier, name, pos) =>
- (SOME (strict, scope), concealed, prefix, qualifier, name, pos));
-
-fun restricted_default restricted' =
+fun restricted default =
map_binding (fn (restricted, concealed, prefix, qualifier, name, pos) =>
- (if is_some restricted then restricted else restricted',
- concealed, prefix, qualifier, name, pos));
+ (if is_some restricted then restricted else default, concealed, prefix, qualifier, name, pos));
val concealed =
map_binding (fn (restricted, _, prefix, qualifier, name, pos) =>
--- a/src/Pure/General/name_space.ML Sun Jan 24 15:02:29 2016 +0100
+++ b/src/Pure/General/name_space.ML Sun Jan 24 15:02:56 2016 +0100
@@ -389,7 +389,7 @@
concealed' ? concealed;
fun transform_binding (Naming {restricted, concealed, ...}) =
- Binding.restricted_default restricted #>
+ Binding.restricted restricted #>
concealed ? Binding.concealed;