changeset 67522 | 9e712280cc37 |
parent 67440 | e5ba0ca1e465 |
child 67532 | 71b36ff8f94d |
--- a/src/Pure/Syntax/lexicon.ML Sun Jan 28 16:09:00 2018 +0100 +++ b/src/Pure/Syntax/lexicon.ML Sun Jan 28 19:28:52 2018 +0100 @@ -406,7 +406,7 @@ let val cs = Symbol.explode str; val (intpart, fracpart) = - (case take_prefix Symbol.is_digit cs of + (case chop_prefix Symbol.is_digit cs of (intpart, "." :: fracpart) => (intpart, fracpart) | _ => raise Fail "read_float"); in