src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML
changeset 33906 1eebf19b773e
parent 33069 d284306ea923
child 35408 b48ab741683b
     1.1 --- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Thu Nov 26 15:28:42 2009 +0100
     1.2 +++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Thu Nov 26 20:07:02 2009 +0100
     1.3 @@ -537,8 +537,8 @@
     1.4   fun token s =
     1.5    Scan.repeat ($$ " ") |-- word s --| Scan.repeat ($$ " ")
     1.6   val numeral = Scan.one isnum
     1.7 - val decimalint = Scan.repeat numeral >> (rat_of_string o implode)
     1.8 - val decimalfrac = Scan.repeat numeral
     1.9 + val decimalint = Scan.repeat1 numeral >> (rat_of_string o implode)
    1.10 + val decimalfrac = Scan.repeat1 numeral
    1.11      >> (fn s => rat_of_string(implode s) // pow10 (length s))
    1.12   val decimalsig =
    1.13      decimalint -- Scan.option (Scan.$$ "." |-- decimalfrac)