# HG changeset patch
# User wenzelm
# Date 1117963885 -7200
# Node ID bd1b38f57fc774a7d1980007ae34a3387c33f973
# Parent  28803c418b59c2a073b9376a96317c7bf3e91664
no warning for non-identifiers;

diff -r 28803c418b59 -r bd1b38f57fc7 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Sun Jun 05 11:31:24 2005 +0200
+++ b/src/Pure/General/name_space.ML	Sun Jun 05 11:31:25 2005 +0200
@@ -215,8 +215,6 @@
     let val names = unpack name in
       conditional (null names orelse exists (equal "") names) (fn () =>
         error ("Bad name declaration " ^ quote name));
-      conditional (exists (not o Symbol.is_ident o Symbol.explode) names) (fn () =>
-        warning ("Declared non-identifier " ^ quote name));
       fold (add_name name) (map pack (accs names)) space
     end;