tuned message;
authorwenzelm
Sat, 04 Apr 2015 21:30:58 +0200
changeset 59925 32402fe5ae6a
parent 59924 801b979ec0c2
child 59926 003dbac78546
tuned message;
src/Pure/General/name_space.ML
--- 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));