eliminated private clones of List.partition;

--- a/src/HOL/Library/reflection.ML	Fri Feb 27 16:54:49 2009 +0100
+++ b/src/HOL/Library/reflection.ML	Fri Feb 27 18:03:47 2009 +0100
@@ -88,17 +88,12 @@
 
 fun dest_listT (Type ("List.list", [T])) = T;
 
-fun partition P [] = ([],[])
-  | partition P (x::xs) = 
-     let val (yes,no) = partition P xs
-     in if P x then (x::yes,no) else (yes, x::no) end
-
 fun rearrange congs = 
 let 
  fun P (_, th) = 
   let val @{term "Trueprop"}$(Const ("op =",_) $l$_) = concl_of th
   in can dest_Var l end
- val (yes,no) = partition P congs 
+ val (yes,no) = List.partition P congs 
  in no @ yes end
 
 fun genreif ctxt raw_eqs t =

--- a/src/HOL/Tools/Qelim/langford.ML	Fri Feb 27 16:54:49 2009 +0100
+++ b/src/HOL/Tools/Qelim/langford.ML	Fri Feb 27 18:03:47 2009 +0100
@@ -113,11 +113,6 @@
   val eqI = instantiate' [] [SOME ll, SOME rr] @{thm iffI}
  in implies_elim (implies_elim eqI thl) thr |> mk_meta_eq end;
 
-fun partition f [] = ([],[])
-  | partition f (x::xs) = 
-      let val (yes,no) = partition f xs 
-      in if f x then (x::yes,no) else (yes, x::no) end;
-
 fun contains x ct = member (op aconv) (OldTerm.term_frees (term_of ct)) (term_of x);
 
 fun is_eqx x eq = case term_of eq of
@@ -132,11 +127,11 @@
     val e = Thm.dest_fun ct
     val (x,p) = Thm.dest_abs (SOME xn) (Thm.dest_arg ct)
     val Pp = Thm.capply @{cterm "Trueprop"} p 
-    val (eqs,neqs) = partition (is_eqx x) (all_conjuncts p)
+    val (eqs,neqs) = List.partition (is_eqx x) (all_conjuncts p)
    in case eqs of
       [] => 
         let 
-         val (dx,ndx) = partition (contains x) neqs
+         val (dx,ndx) = List.partition (contains x) neqs
          in case ndx of [] => NONE
                       | _ =>
             conj_aci_rule (Thm.mk_binop @{cterm "op == :: prop => _"} Pp