# HG changeset patch
# User wenzelm
# Date 1256217975 -7200
# Node ID c39f6bd5a46b1799816646db058ec166a574f273
# Parent  31e928d5653d64ca4aaa48ba96caeb5f463e2480# Parent  d284306ea923f3038006cb11f4677a8d76ae0b62
merged

diff -r 31e928d5653d -r c39f6bd5a46b src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML
--- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Thu Oct 22 15:22:41 2009 +0200
+++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Thu Oct 22 15:26:15 2009 +0200
@@ -537,8 +537,8 @@
  fun token s =
   Scan.repeat ($$ " ") |-- word s --| Scan.repeat ($$ " ")
  val numeral = Scan.one isnum
- val decimalint = Scan.bulk numeral >> (rat_of_string o implode)
- val decimalfrac = Scan.bulk numeral
+ val decimalint = Scan.repeat numeral >> (rat_of_string o implode)
+ val decimalfrac = Scan.repeat numeral
     >> (fn s => rat_of_string(implode s) // pow10 (length s))
  val decimalsig =
     decimalint -- Scan.option (Scan.$$ "." |-- decimalfrac)
@@ -564,7 +564,9 @@
 (* Parse back csdp output.                                                      *)
 
  fun ignore inp = ((),[])
- fun csdpoutput inp =  ((decimal -- Scan.bulk (Scan.$$ " " |-- Scan.option decimal) >> (fn (h,to) => map_filter I ((SOME h)::to))) --| ignore >> vector_of_list) inp
+ fun csdpoutput inp =
+   ((decimal -- Scan.repeat (Scan.$$ " " |-- Scan.option decimal) >>
+    (fn (h,to) => map_filter I ((SOME h)::to))) --| ignore >> vector_of_list) inp
  val parse_csdpoutput = mkparser csdpoutput
 
 (* Run prover on a problem in linear form.                       *)