# HG changeset patch
# User webertj
# Date 1157557192 -7200
# Node ID 02ca20e33030f346dc5133c265268a93530eecb4
# Parent  3078fd2eec7bd3d7d6b8d1786947c37ed5ddfbbe
rawsat_thm: mk_conjunction_list replaced by Conjunction.mk_conjunction_list

diff -r 3078fd2eec7b -r 02ca20e33030 src/HOL/Tools/sat_funcs.ML
--- a/src/HOL/Tools/sat_funcs.ML	Wed Sep 06 13:48:02 2006 +0200
+++ b/src/HOL/Tools/sat_funcs.ML	Wed Sep 06 17:39:52 2006 +0200
@@ -315,11 +315,8 @@
 				(* optimization: convert the given clauses from "[c_i] |- c_i" to *)
 				(* "[c_1 && ... && c_n] |- c_i"; this avoids accumulation of      *)
 				(* hypotheses during resolution                                   *)
-				(* Thm.cterm list -> Thm.cterm *)
-				fun mk_conjunction_list [x]     = x
-				  | mk_conjunction_list (x::xs) = Conjunction.mk_conjunction (x, mk_conjunction_list xs)
 				(* [c_1 && ... && c_n] |- c_1 && ... && c_n *)
-				val cnf_cterm = mk_conjunction_list (map cprop_of non_triv_clauses)
+				val cnf_cterm = Conjunction.mk_conjunction_list (map cprop_of non_triv_clauses)
 				val cnf_thm   = Thm.assume cnf_cterm
 				(* cf. Conjunction.elim_list *)
 				fun right_elim_list th =