diff -r 64bbbd858c39 -r 3ee4c29ead7f src/HOL/Lazy_Sequence.thy
--- a/src/HOL/Lazy_Sequence.thy	Mon Mar 29 17:30:36 2010 +0200
+++ b/src/HOL/Lazy_Sequence.thy	Mon Mar 29 17:30:38 2010 +0200
@@ -131,6 +131,7 @@
   datatype 'a lazy_sequence = Lazy_Sequence of unit -> ('a * 'a lazy_sequence) option
   val yield : 'a lazy_sequence -> ('a * 'a lazy_sequence) option
   val yieldn : int -> 'a lazy_sequence -> ('a list * 'a lazy_sequence)
+  val map : ('a -> 'b) -> 'a lazy_sequence -> 'b lazy_sequence
 end;
 
 structure Lazy_Sequence : LAZY_SEQUENCE =
@@ -142,6 +143,8 @@
 
 val yieldn = @{code yieldn}
 
+val map = @{code map}
+
 end;
 *}