diff -r d5713db7e146 -r dd7490fdd998 Nominal/nominal_library.ML
--- a/Nominal/nominal_library.ML	Sun Dec 19 07:50:37 2010 +0000
+++ b/Nominal/nominal_library.ML	Tue Dec 21 10:28:08 2010 +0000
@@ -10,6 +10,7 @@
   val order: ('a * 'a -> bool) -> 'a list -> ('a * 'b) list -> 'b list
   val remove_dups: ('a * 'a -> bool) -> 'a list -> 'a list
   val partitions: 'a list -> int list -> 'a list list
+  val split_filter: ('a -> bool) -> 'a list -> 'a list * 'a list
 
   val is_true: term -> bool
  
@@ -146,6 +147,15 @@
         head :: partitions tail js
       end
 
+fun split_filter f [] = ([], [])
+  | split_filter f (x :: xs) =
+      let 
+        val (r, l) = split_filter f xs 
+      in 
+        if f x 
+        then (x :: r, l) 
+        else (r, x :: l) 
+      end
 
 
 fun is_true @{term "Trueprop True"} = true