# HG changeset patch # User wenzelm # Date 1428175858 -7200 # Node ID 32402fe5ae6a3b7456b1be94dda0ad19771556c4 # Parent 801b979ec0c2e14e91ff3dbcacf5cdeb2fc8d30c tuned message; diff -r 801b979ec0c2 -r 32402fe5ae6a 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));