# HG changeset patch
# User webertj
# Date 1157159427 -7200
# Node ID 2b3fc1459ffa519c72f00a787372988f89ffed40
# Parent  062c4e9bf3bbb5159e4a3a4f67b251aca9a572db
tuned

diff -r 062c4e9bf3bb -r 2b3fc1459ffa src/HOL/Tools/sat_funcs.ML
--- a/src/HOL/Tools/sat_funcs.ML	Sat Sep 02 01:10:10 2006 +0200
+++ b/src/HOL/Tools/sat_funcs.ML	Sat Sep 02 03:10:27 2006 +0200
@@ -324,7 +324,7 @@
 				(* cf. Conjunction.elim_list *)
 				fun right_elim_list th =
 					let val (th1, th2) = Conjunction.elim th
-					in [th1] @ right_elim_list th2 end handle THM _ => [th]
+					in th1 :: right_elim_list th2 end handle THM _ => [th]
 				(* [[c_1 && ... && c_n] |- c_1, ..., [c_1 && ... && c_n] |- c_n] *)
 				val converted_clauses = right_elim_list cnf_thm
 				(* initialize the clause array with the given clauses *)