declare: disallow quote (") in names;

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