--- 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 =