# HG changeset patch
# User wenzelm
# Date 1153154557 -7200
# Node ID 6dc6fc8b261e8a5d86d24dfd62a510aa5d0a4d45
# Parent  6c04453ac1bd4df5a3d2da0ccf08cae4edf19ffb
replaced butlast by Library.split_last;
removed dead code;

diff -r 6c04453ac1bd -r 6dc6fc8b261e src/HOL/Tools/ATP/recon_order_clauses.ML
--- a/src/HOL/Tools/ATP/recon_order_clauses.ML	Mon Jul 17 15:16:17 2006 +0200
+++ b/src/HOL/Tools/ATP/recon_order_clauses.ML	Mon Jul 17 18:42:37 2006 +0200
@@ -20,16 +20,6 @@
 exception Not_in_list;  
 
 
-fun numlist 0 = []
-|   numlist n = (numlist (n - 1))@[n]
-
-fun butlast []= []
-|   butlast(x::xs) = if xs=[] then [] else (x::(butlast xs))
-
-
-fun minus a b = b - a;
-
-
 (* code to rearrange clauses so that they're the same as the parsed in SPASS version *)
 
  fun takeUntil ch [] res  = (res, [])
@@ -48,12 +38,12 @@
                        then 
                            let val (left, right) = takeUntil "=" str []
                            in
-                               (butlast left, tl right)
+                               (#1 (split_last left), tl right)
                            end
                        else                  (* is an inequality *)
                            let val (left, right) = takeUntil "~" str []
                            in 
-                              (butlast left, tl (tl right))
+                              (#1 (split_last left), tl (tl right))
                            end
                 
 
@@ -69,10 +59,7 @@
 fun var_equiv vars (a,b)  = a=b orelse (is_var_pair (a,b) vars)
 
 fun all_true [] = false
-|   all_true xs = let val falselist = List.filter (equal false ) xs 
-                  in
-                      falselist = []
-                  end
+|   all_true xs = null (List.filter (equal false ) xs)