src/Pure/General/name_space.ML
changeset 16262 bd1b38f57fc7
parent 16137 00e9ca1e7261
child 16341 e573e5167eda
     1.1 --- a/src/Pure/General/name_space.ML	Sun Jun 05 11:31:24 2005 +0200
     1.2 +++ b/src/Pure/General/name_space.ML	Sun Jun 05 11:31:25 2005 +0200
     1.3 @@ -215,8 +215,6 @@
     1.4      let val names = unpack name in
     1.5        conditional (null names orelse exists (equal "") names) (fn () =>
     1.6          error ("Bad name declaration " ^ quote name));
     1.7 -      conditional (exists (not o Symbol.is_ident o Symbol.explode) names) (fn () =>
     1.8 -        warning ("Declared non-identifier " ^ quote name));
     1.9        fold (add_name name) (map pack (accs names)) space
    1.10      end;
    1.11