# HG changeset patch
# User huffman
# Date 1120153430 -7200
# Node ID 78b32293a8b19f2b73c7e493690f1585cceb4b17
# Parent  2a7f46324218f6bdd149b16c4c8a86adf7dd7bc3
replace filter2 with List.partition

diff -r 2a7f46324218 -r 78b32293a8b1 src/HOLCF/cont_consts.ML
--- a/src/HOLCF/cont_consts.ML	Thu Jun 30 14:06:29 2005 +0200
+++ b/src/HOLCF/cont_consts.ML	Thu Jun 30 19:43:50 2005 +0200
@@ -27,12 +27,6 @@
 fun upd_second f (x,y,z) = (  x, f y,   z);
 fun upd_third  f (x,y,z) = (  x,   y, f z);
 
-fun filter2 (pred: 'a->bool) : 'a list -> 'a list * 'a list =
-  let fun filt []      = ([],[])
-        | filt (x::xs) = let val (ys,zs) = filt xs in
-                         if pred x then (x::ys,zs) else (ys,x::zs) end
-  in filt end;
-
 fun change_arrow 0 T               = T
 |   change_arrow n (Type(_,[S,T])) = Type ("fun",[S,change_arrow (n-1) T])
 |   change_arrow _ _               = sys_error "cont_consts: change_arrow";
@@ -87,7 +81,7 @@
 fun gen_add_consts prep_typ raw_decls thy =
   let
     val decls = map (upd_second (Thm.typ_of o prep_typ (Theory.sign_of thy))) raw_decls;
-    val (contconst_decls, normal_decls) = filter2 is_contconst decls;
+    val (contconst_decls, normal_decls) = List.partition is_contconst decls;
     val transformed_decls = map transform contconst_decls;
   in
     thy