# HG changeset patch
# User wenzelm
# Date 1083211503 -7200
# Node ID edb7dacde656fbb230653b33f53ccd6bc729d078
# Parent  e089757b952a68c99e290d75d4fa62fc26fdaeb3
warning: non-identifier declaration;

diff -r e089757b952a -r edb7dacde656 src/Pure/sign.ML
--- 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;