--- a/src/HOL/Tools/ATP/recon_order_clauses.ML Tue Apr 12 13:38:08 2005 +0200
+++ b/src/HOL/Tools/ATP/recon_order_clauses.ML Wed Apr 13 09:48:41 2005 +0200
@@ -1,5 +1,3 @@
-
-
(*----------------------------------------------*)
(* Reorder clauses for use in binary resolution *)
(*----------------------------------------------*)
@@ -7,9 +5,6 @@
fun drop n [] = []
| drop n (x::xs) = (if n = 0 then (x::xs) else drop (n-1) xs)
-fun remove n [] = []
-| remove n (x::xs) = List.filter (not_equal n) (x::xs);
-
fun remove_nth n [] = []
| remove_nth n xs = (List.take (xs, n-1)) @ (List.drop (xs, n))