# HG changeset patch # User wenzelm # Date 1184013657 -7200 # Node ID 8b5a2a79a6e38b044825d66f5da5a32e07d8652d # Parent a4e93948f72ac2d81771326f1a6bf088e0a85a2c declare: disallow quote (") in names; diff -r a4e93948f72a -r 8b5a2a79a6e3 src/Pure/General/name_space.ML --- a/src/Pure/General/name_space.ML Mon Jul 09 22:37:48 2007 +0200 +++ b/src/Pure/General/name_space.ML Mon Jul 09 22:40:57 2007 +0200 @@ -227,7 +227,8 @@ else let val names = explode_name name; - val _ = (null names orelse exists (fn s => s = "") names) andalso + val _ = (null names orelse exists (fn s => s = "") names + orelse exists_string (fn s => s = "\"") name) andalso error ("Bad name declaration " ^ quote name); in fold (add_name name) (map implode_name (accs names)) space end;