1.1 --- a/src/HOL/DSequence.thy	Thu Nov 15 17:36:08 2012 +0100
     1.2 +++ b/src/HOL/DSequence.thy	Thu Nov 15 12:11:15 2012 +0100
     1.3 @@ -27,6 +27,12 @@
     1.4      None => None
     1.5    | Some s => Option.map (apsnd (%r i pol. Some r)) (Lazy_Sequence.yield s))"
     1.6  
     1.7 +definition yieldn :: "code_numeral \<Rightarrow> 'a dseq \<Rightarrow> code_numeral \<Rightarrow> bool \<Rightarrow> 'a list \<times> 'a dseq"
     1.8 +where
     1.9 +  "yieldn n dseq i pol = (case dseq i pol of
    1.10 +    None \<Rightarrow> ([], \<lambda>i pol. None)
    1.11 +  | Some s \<Rightarrow> let (xs, s') = Lazy_Sequence.yieldn n s in (xs, \<lambda>i pol. Some s'))"
    1.12 +
    1.13  fun map_seq :: "('a => 'b dseq) => 'a Lazy_Sequence.lazy_sequence => 'b dseq"
    1.14  where
    1.15    "map_seq f xq i pol = (case Lazy_Sequence.yield xq of
    1.16 @@ -86,10 +92,7 @@
    1.17  type 'a dseq = int -> bool -> 'a Lazy_Sequence.lazy_sequence option
    1.18  
    1.19  val yield = @{code yield}
    1.20 -fun yieldn n s d pol = case s d pol of  
    1.21 -    NONE => ([], fn d => fn pol => NONE)
    1.22 -  | SOME s => let val (xs, s') = Lazy_Sequence.yieldn n s in (xs, fn d => fn pol => SOME s') end
    1.23 -
    1.24 +val yieldn = @{code yieldn}
    1.25  val map = @{code map}
    1.26  
    1.27  end;
    1.28 @@ -107,3 +110,4 @@
    1.29    if_seq_def not_seq_def map_def
    1.30  
    1.31  end
    1.32 +