src/Pure/Syntax/syn_ext.ML

--- a/src/Pure/Syntax/syn_ext.ML	Mon May 18 17:57:16 1998 +0200
+++ b/src/Pure/Syntax/syn_ext.ML	Mon May 18 17:57:47 1998 +0200
@@ -189,7 +189,7 @@
     $$ "'" -- Scan.one Symbol.is_blank >> K None;
 
   val scan_symbs = Scan.repeat scan_symb --| Scan.ahead (Scan.one (not_equal "'"));
-  val read_symbs = mapfilter I o #1 o Scan.error (Scan.finite Symbol.eof scan_symbs);
+  val read_symbs = mapfilter I o #1 o Scan.error (Scan.finite Symbol.stopper scan_symbs);
 in
   val read_mixfix = read_symbs o Symbol.explode;
 end;