no warning for non-identifiers;

--- 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;