diff -r 3e677ca1e564 -r 70096cbdd4e0 src/HOL/Lazy_Sequence.thy
--- a/src/HOL/Lazy_Sequence.thy	Wed Apr 28 15:42:10 2010 +0200
+++ b/src/HOL/Lazy_Sequence.thy	Wed Apr 28 16:56:18 2010 +0200
@@ -123,6 +123,13 @@
 
 subsection {* Code setup *}
 
+code_reflect
+  datatypes lazy_sequence = Lazy_Sequence
+  functions "Lazy_Sequence.map" yield
+  module_name Lazy_Sequence
+
+(* FIXME formulate yieldn in the logic with type code_numeral *)
+
 ML {*
 signature LAZY_SEQUENCE =
 sig
@@ -135,9 +142,9 @@
 structure Lazy_Sequence : LAZY_SEQUENCE =
 struct
 
-@{code_datatype lazy_sequence = Lazy_Sequence}
+open Lazy_Sequence;
 
-val yield = @{code yield}
+fun map f = mapa f;
 
 fun anamorph f k x = (if k = 0 then ([], x)
   else case f x
@@ -148,17 +155,9 @@
 
 fun yieldn S = anamorph yield S;
 
-val map = @{code map}
-
 end;
 *}
 
-code_reserved Eval Lazy_Sequence
-
-code_type lazy_sequence (Eval "_/ Lazy'_Sequence.lazy'_sequence")
-
-code_const Lazy_Sequence (Eval "Lazy'_Sequence.Lazy'_Sequence")
-
 section {* With Hit Bound Value *}
 text {* assuming in negative context *}