changeset 27799 | 52f07d5292cd |
parent 27772 | b933c997eab3 |
child 27817 | 78cae5cca09e |
--- a/src/Pure/ML/ml_lex.ML Sat Aug 09 00:09:31 2008 +0200 +++ b/src/Pure/ML/ml_lex.ML Sat Aug 09 00:09:34 2008 +0200 @@ -184,9 +184,7 @@ local -fun token k s = - let val (x, range) = SymbolPos.implode s - in Token (range, (k, x)) end; +fun token k ss = Token (SymbolPos.range ss, (k, SymbolPos.implode ss)); val scan = !!! "bad input" (scan_char >> token Char ||