src/HOL/Lazy_Sequence.thy
changeset 36516 8dac276ab10d
parent 36513 70096cbdd4e0
child 36533 f8df589ca2a5
--- a/src/HOL/Lazy_Sequence.thy	Wed Apr 28 16:56:19 2010 +0200
+++ b/src/HOL/Lazy_Sequence.thy	Wed Apr 28 17:04:56 2010 +0200
@@ -125,10 +125,10 @@
 
 code_reflect
   datatypes lazy_sequence = Lazy_Sequence
-  functions "Lazy_Sequence.map" yield
+  functions map yield
   module_name Lazy_Sequence
 
-(* FIXME formulate yieldn in the logic with type code_numeral *)
+(* FIXME formulate yieldn in the logic with type code_numeral -- get rid of mapa confusion *)
 
 ML {*
 signature LAZY_SEQUENCE =
@@ -137,6 +137,7 @@
   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
+  val mapa : ('a -> 'b) -> 'a lazy_sequence -> 'b lazy_sequence
 end;
 
 structure Lazy_Sequence : LAZY_SEQUENCE =