butlast removed (use fst o split_last instead)
authorwebertj
Mon Jul 17 15:16:17 2006 +0200 (2006-07-17)
changeset 201376c04453ac1bd
parent 20136 8e92a8f9720b
child 20138 6dc6fc8b261e
butlast removed (use fst o split_last instead)
src/HOL/Tools/sat_solver.ML
src/Pure/library.ML
     1.1 --- a/src/HOL/Tools/sat_solver.ML	Mon Jul 17 01:28:17 2006 +0200
     1.2 +++ b/src/HOL/Tools/sat_solver.ML	Mon Jul 17 15:16:17 2006 +0200
     1.3 @@ -699,7 +699,7 @@
     1.4  							val cid      = int_from_string id
     1.5  							val _        = if sep = "<=" then () else raise INVALID_PROOF ("File format error: \"<=\" expected (" ^ quote sep ^ " encountered).")
     1.6  							val zero     = List.last lits handle List.Empty => raise INVALID_PROOF "File format error: \"R\" not terminated by \"0\"."
     1.7 -							val ls       = sort int_ord (map int_from_string (butlast lits))
     1.8 +							val ls       = sort int_ord (map int_from_string ((fst o split_last) lits))
     1.9  							val _        = if zero = "0" then () else raise INVALID_PROOF ("File format error: \"0\" expected (" ^ quote zero ^ " encountered).")
    1.10  							val proof_id = (* both 'ls' and the list of literals used as key in 'clauses' are sorted, *)
    1.11  							               (* so testing for equality should suffice -- barring duplicate literals    *)
    1.12 @@ -727,7 +727,7 @@
    1.13  							fun unevens []             = raise INVALID_PROOF "File format error: \"C\" followed by an even number of IDs."
    1.14  							  | unevens (x :: [])      = x :: []
    1.15  							  | unevens (x :: _ :: xs) = x :: unevens xs
    1.16 -							val rs       = (map sat_to_proof o unevens o map int_from_string o butlast) ids
    1.17 +							val rs       = (map sat_to_proof o unevens o map int_from_string o fst o split_last) ids
    1.18  							val _        = if dot = "." then () else raise INVALID_PROOF ("File format error: \".\" expected (" ^ quote dot ^ " encountered).")
    1.19  							(* extend the mapping of clause IDs with this newly defined ID *)
    1.20  							val proof_id = inc next_id
     2.1 --- a/src/Pure/library.ML	Mon Jul 17 01:28:17 2006 +0200
     2.2 +++ b/src/Pure/library.ML	Mon Jul 17 15:16:17 2006 +0200
     2.3 @@ -103,7 +103,6 @@
     2.4    val cons: 'a -> 'a list -> 'a list
     2.5    val single: 'a -> 'a list
     2.6    val singleton: ('a list -> 'b list) -> 'a -> 'b
     2.7 -  val butlast: 'a list -> 'a list
     2.8    val append: 'a list -> 'a list -> 'a list
     2.9    val apply: ('a -> 'a) list -> 'a -> 'a
    2.10    val fold: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
    2.11 @@ -497,10 +496,6 @@
    2.12  
    2.13  fun singleton f x = (case f [x] of [y] => y | _ => raise Empty);
    2.14  
    2.15 -fun butlast []        = raise Empty
    2.16 -  | butlast (x :: []) = []
    2.17 -  | butlast (x :: xs) = x :: butlast xs;
    2.18 -
    2.19  fun append xs ys = xs @ ys;
    2.20  
    2.21  fun apply [] x = x