new in mixfix annotations: "' " (quote space) separates delimiters without
adding extra white space for printing;

--- a/doc-src/Ref/defining.tex	Mon Feb 27 17:47:44 1995 +0100
+++ b/doc-src/Ref/defining.tex	Mon Feb 27 17:47:57 1995 +0100
@@ -458,7 +458,7 @@
 is taken into account).  Finally, the nonterminal of a type variable is {\tt
 any}.
 
-\begin{warn} 
+\begin{warn}
   Theories must sometimes declare types for purely syntactic purposes ---
   merely playing the role of nonterminals. One example is \tydx{type}, the
   built-in type of types.  This is a `type of all types' in the syntactic
@@ -480,10 +480,10 @@
 Chapter~\ref{chap:syntax}).
 
 
-\medskip 
-As a special case of the general mixfix declaration, the form 
+\medskip
+As a special case of the general mixfix declaration, the form
 \begin{center}
-  {\tt $c$ ::\ "$\sigma$" ("$template$")} 
+  {\tt $c$ ::\ "$\sigma$" ("$template$")}
 \end{center}
 specifies no priorities.  The resulting production puts no priority
 constraints on any of its arguments and has maximal priority itself.
@@ -560,7 +560,8 @@
   other than the special characters {\tt _}, {\tt(}, {\tt)} and~{\tt/}.
   Even these characters may appear if escaped; this means preceding it with
   a~{\tt '} (single quote).  Thus you have to write {\tt ''} if you really
-  want a single quote.  Delimiters may never contain spaces.
+  want a single quote.  Furthermore, a~{\tt '} followed by a space separates
+  delimiters without extra white space being added for printing.
 
 \item[~{\tt_}~] is an argument position, which stands for a nonterminal symbol
   or name token.

--- a/src/Pure/Syntax/syn_ext.ML	Mon Feb 27 17:47:44 1995 +0100
+++ b/src/Pure/Syntax/syn_ext.ML	Mon Feb 27 17:47:57 1995 +0100
@@ -1,6 +1,6 @@
 (*  Title:      Pure/Syntax/syn_ext.ML
     ID:         $Id$
-    Author:     Markus Wenzel, TU Muenchen
+    Author:     Markus Wenzel and Carsten Clasohm, TU Muenchen
 
 Syntax extension (internal interface).
 *)
@@ -186,23 +186,31 @@
       else err "unbalanced block parentheses";
 
 
-    fun is_meta c = c mem ["(", ")", "/", "_"];
+    local
+      fun is_meta c = c mem ["(", ")", "/", "_"];
 
-    fun scan_delim_char ("'" :: c :: cs) =
-          if is_blank c then err "illegal spaces in delimiter" else (c, cs)
-      | scan_delim_char ["'"] = err "trailing escape character"
-      | scan_delim_char (chs as c :: cs) =
-          if is_blank c orelse is_meta c then raise LEXICAL_ERROR else (c, cs)
-      | scan_delim_char [] = raise LEXICAL_ERROR;
+      fun scan_delim_char ("'" :: c :: cs) =
+            if is_blank c then raise LEXICAL_ERROR else (c, cs)
+        | scan_delim_char ["'"] = err "trailing escape character"
+        | scan_delim_char (chs as c :: cs) =
+            if is_blank c orelse is_meta c then raise LEXICAL_ERROR else (c, cs)
+        | scan_delim_char [] = raise LEXICAL_ERROR;
 
-    val scan_symb =
-      $$ "_" >> K (Argument ("", 0)) ||
-      $$ "(" -- scan_int >> (Bg o #2) ||
-      $$ ")" >> K En ||
-      $$ "/" -- $$ "/" >> K (Brk ~1) ||
-      $$ "/" -- scan_any is_blank >> (Brk o length o #2) ||
-      scan_any1 is_blank >> (Space o implode) ||
-      repeat1 scan_delim_char >> (Delim o implode);
+      val scan_sym =
+        $$ "_" >> K (Argument ("", 0)) ||
+        $$ "(" -- scan_int >> (Bg o #2) ||
+        $$ ")" >> K En ||
+        $$ "/" -- $$ "/" >> K (Brk ~1) ||
+        $$ "/" -- scan_any is_blank >> (Brk o length o #2) ||
+        scan_any1 is_blank >> (Space o implode) ||
+        repeat1 scan_delim_char >> (Delim o implode);
+
+      val scan_symb =
+        scan_sym >> Some ||
+        $$ "'" -- scan_one is_blank >> K None;
+    in
+      val scan_symbs = mapfilter I o #1 o repeat scan_symb;
+    end;
 
 
     val cons_fst = apfst o cons;
@@ -237,7 +245,7 @@
           else a
       | unify_logtypes _ a = a;
 
-    val (raw_symbs, _) = repeat scan_symb (explode sy);
+    val raw_symbs = scan_symbs (explode sy);
     val (symbs, lhs) = add_args raw_symbs typ pris;
     val copy_prod = lhs mem ["prop", "logic"]
           andalso const <> ""