| changeset 62241 | a4a1f282bcd5 |
| parent 60924 | 610794dff23c |
| child 62967 | 5e8b1aead28f |
--- 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;