replaced butlast by Library.split_last;

--- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Mon Jul 17 18:42:37 2006 +0200
+++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Mon Jul 17 18:42:38 2006 +0200
@@ -613,8 +613,7 @@
 	val axioms = get_axioms axioms_and_steps
 	
 	val steps = Library.drop (origax_num, axioms_and_steps)
-	val firststeps = ReconOrderClauses.butlast steps
-	val laststep = List.last steps
+	val (firststeps, laststep) = split_last steps
 	
 	val isar_proof = 
 		("show \"[your goal]\"\n")^