src/HOL/Predicate.thy

 sig
   datatype 'a pred = Seq of (unit -> 'a seq)
   and 'a seq = Empty | Insert of 'a * 'a pred | Join of 'a pred * 'a seq
   val yield: 'a pred -> ('a * 'a pred) option
   val yieldn: int -> 'a pred -> 'a list * 'a pred
+  val map: ('a -> 'b) -> 'a pred -> 'b pred
 end;
 
 structure Predicate : PREDICATE =
 struct
 

     | SOME (v, y) => let
         val (vs, z) = anamorph f (k - 1) y
       in (v :: vs, z) end)
 
 fun yieldn P = anamorph yield P;
+
+fun map f = @{code map} f;
 
 end;
 *}
 
 code_reserved Eval Predicate