changeset 50637 | 81d6fe75ea5b |
parent 48902 | 44a6967240b7 |
child 50913 | 697e3bb60a3b |
--- a/src/Pure/library.ML Sun Dec 30 16:23:30 2012 +0100 +++ b/src/Pure/library.ML Sun Dec 30 16:33:05 2012 +0100 @@ -668,9 +668,9 @@ val limit = zero + radix; fun scan (num, []) = (num, []) | scan (num, c :: cs) = - if zero <= ord c andalso ord c < limit then - scan (radix * num + (ord c - zero), cs) - else (num, c :: cs); + if zero <= ord c andalso ord c < limit then + scan (radix * num + (ord c - zero), cs) + else (num, c :: cs); in scan (0, cs) end; val read_int = read_radix_int 10;