# HG changeset patch
# User haftmann
# Date 1272467096 -7200
# Node ID 8dac276ab10d698c58aaa9342a71f80f85965a0d
# Parent  4073bf588746c7694ea0fd99d47e7a8f135c89f4
export somehow odd mapa explicitly

diff -r 4073bf588746 -r 8dac276ab10d src/HOL/Lazy_Sequence.thy
--- 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 =