--- a/src/HOL/Tools/sat_solver.ML Mon Jul 17 01:28:17 2006 +0200
+++ b/src/HOL/Tools/sat_solver.ML Mon Jul 17 15:16:17 2006 +0200
@@ -699,7 +699,7 @@
val cid = int_from_string id
val _ = if sep = "<=" then () else raise INVALID_PROOF ("File format error: \"<=\" expected (" ^ quote sep ^ " encountered).")
val zero = List.last lits handle List.Empty => raise INVALID_PROOF "File format error: \"R\" not terminated by \"0\"."
- val ls = sort int_ord (map int_from_string (butlast lits))
+ val ls = sort int_ord (map int_from_string ((fst o split_last) lits))
val _ = if zero = "0" then () else raise INVALID_PROOF ("File format error: \"0\" expected (" ^ quote zero ^ " encountered).")
val proof_id = (* both 'ls' and the list of literals used as key in 'clauses' are sorted, *)
(* so testing for equality should suffice -- barring duplicate literals *)
@@ -727,7 +727,7 @@
fun unevens [] = raise INVALID_PROOF "File format error: \"C\" followed by an even number of IDs."
| unevens (x :: []) = x :: []
| unevens (x :: _ :: xs) = x :: unevens xs
- val rs = (map sat_to_proof o unevens o map int_from_string o butlast) ids
+ val rs = (map sat_to_proof o unevens o map int_from_string o fst o split_last) ids
val _ = if dot = "." then () else raise INVALID_PROOF ("File format error: \".\" expected (" ^ quote dot ^ " encountered).")
(* extend the mapping of clause IDs with this newly defined ID *)
val proof_id = inc next_id
--- a/src/Pure/library.ML Mon Jul 17 01:28:17 2006 +0200
+++ b/src/Pure/library.ML Mon Jul 17 15:16:17 2006 +0200
@@ -103,7 +103,6 @@
val cons: 'a -> 'a list -> 'a list
val single: 'a -> 'a list
val singleton: ('a list -> 'b list) -> 'a -> 'b
- val butlast: 'a list -> 'a list
val append: 'a list -> 'a list -> 'a list
val apply: ('a -> 'a) list -> 'a -> 'a
val fold: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
@@ -497,10 +496,6 @@
fun singleton f x = (case f [x] of [y] => y | _ => raise Empty);
-fun butlast [] = raise Empty
- | butlast (x :: []) = []
- | butlast (x :: xs) = x :: butlast xs;
-
fun append xs ys = xs @ ys;
fun apply [] x = x