use plain Scan.repeat (NB: Scan.bulk is for cascading sources -- mostly interna use);
authorwenzelm
Wed, 21 Oct 2009 21:15:33 +0200
changeset 33067 a70d5baa53ee
parent 33052 6f071d92960b
child 33068 bee53a9f45c8
use plain Scan.repeat (NB: Scan.bulk is for cascading sources -- mostly interna use);
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.                       *)