changeset 5870 | 5d4fc952be47 |
parent 5229 | 7c8abffc4413 |
child 5909 | 3fc6497f1c7b |
--- 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;