src/Pure/General/seq.ML
changeset 16534 95460b6eb712
parent 16002 e0557c452138
child 17347 fb3d42ef61ed
     1.1 --- a/src/Pure/General/seq.ML	Wed Jun 22 19:41:18 2005 +0200
     1.2 +++ b/src/Pure/General/seq.ML	Wed Jun 22 19:41:19 2005 +0200
     1.3 @@ -151,18 +151,16 @@
     1.4        NONE => pull yq
     1.5      | SOME (x, xq') => SOME (x, interleave (yq, xq'))));
     1.6  
     1.7 -
     1.8 -(*functional to print a sequence, up to "count" elements;
     1.9 -  the function prelem should print the element number and also the element*)
    1.10 -fun print prelem count seq =
    1.11 +(*print a sequence, up to "count" elements*)
    1.12 +fun print print_elem count =
    1.13    let
    1.14 -    fun pr (k, xq) =
    1.15 +    fun prnt k xq =
    1.16        if k > count then ()
    1.17        else
    1.18          (case pull xq of
    1.19            NONE => ()
    1.20 -        | SOME (x, xq') => (prelem k x; writeln ""; pr (k + 1, xq')))
    1.21 -  in pr (1, seq) end;
    1.22 +        | SOME (x, xq') => (print_elem k x; writeln ""; prnt (k + 1) xq'));
    1.23 +  in prnt 1 end;
    1.24  
    1.25  (*accumulating a function over a sequence; this is lazy*)
    1.26  fun it_right f (xq, yq) =