declare: disallow quote (") in names;
authorwenzelm
Mon Jul 09 22:40:57 2007 +0200 (2007-07-09)
changeset 236688b5a2a79a6e3
parent 23667 a4e93948f72a
child 23669 5d3c022cbf97
declare: disallow quote (") in names;
src/Pure/General/name_space.ML
     1.1 --- a/src/Pure/General/name_space.ML	Mon Jul 09 22:37:48 2007 +0200
     1.2 +++ b/src/Pure/General/name_space.ML	Mon Jul 09 22:40:57 2007 +0200
     1.3 @@ -227,7 +227,8 @@
     1.4    else
     1.5      let
     1.6        val names = explode_name name;
     1.7 -      val _ = (null names orelse exists (fn s => s = "") names) andalso
     1.8 +      val _ = (null names orelse exists (fn s => s = "") names
     1.9 +          orelse exists_string (fn s => s = "\"") name) andalso
    1.10          error ("Bad name declaration " ^ quote name);
    1.11      in fold (add_name name) (map implode_name (accs names)) space end;
    1.12