1.1 --- a/src/HOL/Tools/Qelim/langford.ML	Wed Mar 04 10:43:39 2009 +0100
     1.2 +++ b/src/HOL/Tools/Qelim/langford.ML	Wed Mar 04 10:45:52 2009 +0100
     1.3 @@ -113,11 +113,6 @@
     1.4    val eqI = instantiate' [] [SOME ll, SOME rr] @{thm iffI}
     1.5   in implies_elim (implies_elim eqI thl) thr |> mk_meta_eq end;
     1.6  
     1.7 -fun partition f [] = ([],[])
     1.8 -  | partition f (x::xs) = 
     1.9 -      let val (yes,no) = partition f xs 
    1.10 -      in if f x then (x::yes,no) else (yes, x::no) end;
    1.11 -
    1.12  fun contains x ct = member (op aconv) (OldTerm.term_frees (term_of ct)) (term_of x);
    1.13  
    1.14  fun is_eqx x eq = case term_of eq of
    1.15 @@ -132,11 +127,11 @@
    1.16      val e = Thm.dest_fun ct
    1.17      val (x,p) = Thm.dest_abs (SOME xn) (Thm.dest_arg ct)
    1.18      val Pp = Thm.capply @{cterm "Trueprop"} p 
    1.19 -    val (eqs,neqs) = partition (is_eqx x) (all_conjuncts p)
    1.20 +    val (eqs,neqs) = List.partition (is_eqx x) (all_conjuncts p)
    1.21     in case eqs of
    1.22        [] => 
    1.23          let 
    1.24 -         val (dx,ndx) = partition (contains x) neqs
    1.25 +         val (dx,ndx) = List.partition (contains x) neqs
    1.26           in case ndx of [] => NONE
    1.27                        | _ =>
    1.28              conj_aci_rule (Thm.mk_binop @{cterm "op == :: prop => _"} Pp