src/Pure/Syntax/symbol.ML

   | no_syms (c :: cs) = ord c < enc_start andalso no_syms cs;
 
 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;
 
 
 (* printable length *)