src/HOL/Predicate.thy

--- a/src/HOL/Predicate.thy	Wed May 20 22:24:07 2009 +0200
+++ b/src/HOL/Predicate.thy	Thu May 21 09:07:13 2009 +0200
@@ -637,6 +637,7 @@
   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 =
@@ -661,6 +662,8 @@
 
 fun yieldn P = anamorph yield P;
 
+fun map f = @{code map} f;
+
 end;
 *}