warning: non-identifier declaration;

--- a/src/Pure/sign.ML	Thu Apr 29 06:04:01 2004 +0200
+++ b/src/Pure/sign.ML	Thu Apr 29 06:05:03 2004 +0200
@@ -497,7 +497,10 @@
   | full (Some path) name =
       if NameSpace.is_qualified name then
         error ("Attempt to declare qualified name " ^ quote name)
-      else NameSpace.pack (path @ [name]);
+      else
+       (if not (Syntax.is_identifier name)
+        then warning ("Declared non-identifier name " ^ quote name) else ();
+        NameSpace.pack (path @ [name]));
 
 (*base name*)
 val base_name = NameSpace.base;