# HG changeset patch
# User haftmann
# Date 1242889633 -7200
# Node ID 4a84ae57b65fdd3884647cdfbfcde1052885e014
# Parent  fa54c1e614df5d1e988df67b99978a2f4a56c80c
added Predicate.map in SML environment

diff -r fa54c1e614df -r 4a84ae57b65f 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;
 *}