# HG changeset patch
# User wenzelm
# Date 1153154558 -7200
# Node ID 804927db5311d5e0b87177c659c205a1b17c8ef5
# Parent  6dc6fc8b261e8a5d86d24dfd62a510aa5d0a4d45
replaced butlast by Library.split_last;

diff -r 6dc6fc8b261e -r 804927db5311 src/HOL/Tools/ATP/recon_transfer_proof.ML
--- 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")^