# 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;