--- a/src/Pure/General/name_space.ML Sat Apr 04 21:21:40 2015 +0200
+++ b/src/Pure/General/name_space.ML Sat Apr 04 21:30:58 2015 +0200
@@ -335,7 +335,7 @@
fun private pos naming =
(case get_scope naming of
SOME scope => private_scope scope naming
- | NONE => error ("Unknown scope -- cannot declare names private" ^ Position.here pos));
+ | NONE => error ("Missing local scope -- cannot declare private names" ^ Position.here pos));
val concealed = map_naming (fn (scopes, private, _, group, theory_name, path) =>
(scopes, private, true, group, theory_name, path));