--- 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