src/Pure/sign.ML
changeset 14688 edb7dacde656
parent 14645 83776a9f0a9c
child 14700 2f885b7e5ba7
     1.1 --- a/src/Pure/sign.ML	Thu Apr 29 06:04:01 2004 +0200
     1.2 +++ b/src/Pure/sign.ML	Thu Apr 29 06:05:03 2004 +0200
     1.3 @@ -497,7 +497,10 @@
     1.4    | full (Some path) name =
     1.5        if NameSpace.is_qualified name then
     1.6          error ("Attempt to declare qualified name " ^ quote name)
     1.7 -      else NameSpace.pack (path @ [name]);
     1.8 +      else
     1.9 +       (if not (Syntax.is_identifier name)
    1.10 +        then warning ("Declared non-identifier name " ^ quote name) else ();
    1.11 +        NameSpace.pack (path @ [name]));
    1.12  
    1.13  (*base name*)
    1.14  val base_name = NameSpace.base;