# HG changeset patch
# User wenzelm
# Date 911209287 -3600
# Node ID 5d4fc952be47a110b8991c178eba1fd0c1e96c0d
# Parent  b279a84ac11cc703bba8dababb67a2a118c1ceb4
Scan.read;

diff -r b279a84ac11c -r 5d4fc952be47 src/Pure/Syntax/symbol.ML
--- 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;
 
 
diff -r b279a84ac11c -r 5d4fc952be47 src/Pure/Syntax/syn_ext.ML
--- 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;