src/HOL/Tools/ATP/recon_order_clauses.ML
changeset 15702 2677db44c795
parent 15700 970e0293dfb3
child 15739 bb2acfed8212
     1.1 --- a/src/HOL/Tools/ATP/recon_order_clauses.ML	Tue Apr 12 13:38:08 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/recon_order_clauses.ML	Wed Apr 13 09:48:41 2005 +0200
     1.3 @@ -1,5 +1,3 @@
     1.4 -
     1.5 -
     1.6  (*----------------------------------------------*)
     1.7  (* Reorder clauses for use in binary resolution *)
     1.8  (*----------------------------------------------*)
     1.9 @@ -7,9 +5,6 @@
    1.10  fun drop n [] = []
    1.11  |   drop n (x::xs) = (if n = 0 then (x::xs) else drop (n-1) xs)
    1.12  
    1.13 -fun remove n [] = []
    1.14 -|   remove n (x::xs) = List.filter (not_equal n) (x::xs);
    1.15 -
    1.16  fun remove_nth n [] = []
    1.17  |   remove_nth n xs = (List.take (xs, n-1)) @ (List.drop (xs, n))
    1.18