# HG changeset patch
# User Philipp Meyer
# Date 1259262422 -3600
# Node ID 1eebf19b773ef9b74491111a39cdce25f796b9c9
# Parent  5760ba045bf0e891b23cf7784f89333fb45378ef
fixed csdp output parser

diff -r 5760ba045bf0 -r 1eebf19b773e src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML
--- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Thu Nov 26 15:28:42 2009 +0100
+++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Thu Nov 26 20:07:02 2009 +0100
@@ -537,8 +537,8 @@
  fun token s =
   Scan.repeat ($$ " ") |-- word s --| Scan.repeat ($$ " ")
  val numeral = Scan.one isnum
- val decimalint = Scan.repeat numeral >> (rat_of_string o implode)
- val decimalfrac = Scan.repeat numeral
+ val decimalint = Scan.repeat1 numeral >> (rat_of_string o implode)
+ val decimalfrac = Scan.repeat1 numeral
     >> (fn s => rat_of_string(implode s) // pow10 (length s))
  val decimalsig =
     decimalint -- Scan.option (Scan.$$ "." |-- decimalfrac)