Scan.read;

--- a/src/Pure/Syntax/symbol.ML	Mon Nov 16 10:41:08 1998 +0100
+++ b/src/Pure/Syntax/symbol.ML	Mon Nov 16 10:41:27 1998 +0100
@@ -244,7 +244,7 @@
 fun sym_explode str =
   let val chs = explode str in
     if no_syms chs then chs     (*tune trivial case*)
-    else map symbol (#1 (Scan.error (Scan.finite stopper (Scan.repeat scan)) chs))
+    else map symbol (the (Scan.read stopper (Scan.repeat scan) chs))
   end;
 
 

--- a/src/Pure/Syntax/syn_ext.ML	Mon Nov 16 10:41:08 1998 +0100
+++ b/src/Pure/Syntax/syn_ext.ML	Mon Nov 16 10:41:27 1998 +0100
@@ -187,7 +187,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.stopper scan_symbs);
+  val read_symbs = mapfilter I o the o Scan.read Symbol.stopper scan_symbs;
 in
   val read_mixfix = read_symbs o Symbol.explode;
 end;