# HG changeset patch
# User haftmann
# Date 1352977875 -3600
# Node ID 39898c71933982132f6343db8538afe0c0400335
# Parent  b3b5dc2350b7b8c48eb5f4d8e7a3ff198efd5d17
prefer implementation in HOL;
n.b. code_reflect cannot reflect type synonyms

diff -r b3b5dc2350b7 -r 39898c719339 src/HOL/DSequence.thy
--- a/src/HOL/DSequence.thy	Thu Nov 15 17:36:08 2012 +0100
+++ b/src/HOL/DSequence.thy	Thu Nov 15 12:11:15 2012 +0100
@@ -27,6 +27,12 @@
     None => None
   | Some s => Option.map (apsnd (%r i pol. Some r)) (Lazy_Sequence.yield s))"
 
+definition yieldn :: "code_numeral \<Rightarrow> 'a dseq \<Rightarrow> code_numeral \<Rightarrow> bool \<Rightarrow> 'a list \<times> 'a dseq"
+where
+  "yieldn n dseq i pol = (case dseq i pol of
+    None \<Rightarrow> ([], \<lambda>i pol. None)
+  | Some s \<Rightarrow> let (xs, s') = Lazy_Sequence.yieldn n s in (xs, \<lambda>i pol. Some s'))"
+
 fun map_seq :: "('a => 'b dseq) => 'a Lazy_Sequence.lazy_sequence => 'b dseq"
 where
   "map_seq f xq i pol = (case Lazy_Sequence.yield xq of
@@ -86,10 +92,7 @@
 type 'a dseq = int -> bool -> 'a Lazy_Sequence.lazy_sequence option
 
 val yield = @{code yield}
-fun yieldn n s d pol = case s d pol of  
-    NONE => ([], fn d => fn pol => NONE)
-  | SOME s => let val (xs, s') = Lazy_Sequence.yieldn n s in (xs, fn d => fn pol => SOME s') end
-
+val yieldn = @{code yieldn}
 val map = @{code map}
 
 end;
@@ -107,3 +110,4 @@
   if_seq_def not_seq_def map_def
 
 end
+