# HG changeset patch
# User wenzelm
# Date 1453644176 -3600
# Node ID a4a1f282bcd5eab9e8a9fe2f91207a07e3636bfa
# Parent  e099a94290c15cca8fe6bd4f066a37fd43ab226a
tuned signature;
tuned;

diff -r e099a94290c1 -r a4a1f282bcd5 src/Pure/General/binding.ML
--- 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) =>
diff -r e099a94290c1 -r a4a1f282bcd5 src/Pure/General/name_space.ML
--- 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;