# HG changeset patch
# User wenzelm
# Date 1256152533 -7200
# Node ID a70d5baa53ee3b7e8b9d86cff2bb0e9ead6a870d
# Parent  6f071d92960b73a74bbbeea3e0e6e4b0329618f1
use plain Scan.repeat (NB: Scan.bulk is for cascading sources -- mostly interna use);

diff -r 6f071d92960b -r a70d5baa53ee src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML
--- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Wed Oct 21 15:54:31 2009 +0200
+++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Wed Oct 21 21:15:33 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.                       *)