rawsat_thm: mk_conjunction_list replaced by Conjunction.mk_conjunction_list
authorwebertj
Wed Sep 06 17:39:52 2006 +0200 (2006-09-06)
changeset 2048602ca20e33030
parent 20485 3078fd2eec7b
child 20487 6ac7a4fc32a0
rawsat_thm: mk_conjunction_list replaced by Conjunction.mk_conjunction_list
src/HOL/Tools/sat_funcs.ML
     1.1 --- a/src/HOL/Tools/sat_funcs.ML	Wed Sep 06 13:48:02 2006 +0200
     1.2 +++ b/src/HOL/Tools/sat_funcs.ML	Wed Sep 06 17:39:52 2006 +0200
     1.3 @@ -315,11 +315,8 @@
     1.4  				(* optimization: convert the given clauses from "[c_i] |- c_i" to *)
     1.5  				(* "[c_1 && ... && c_n] |- c_i"; this avoids accumulation of      *)
     1.6  				(* hypotheses during resolution                                   *)
     1.7 -				(* Thm.cterm list -> Thm.cterm *)
     1.8 -				fun mk_conjunction_list [x]     = x
     1.9 -				  | mk_conjunction_list (x::xs) = Conjunction.mk_conjunction (x, mk_conjunction_list xs)
    1.10  				(* [c_1 && ... && c_n] |- c_1 && ... && c_n *)
    1.11 -				val cnf_cterm = mk_conjunction_list (map cprop_of non_triv_clauses)
    1.12 +				val cnf_cterm = Conjunction.mk_conjunction_list (map cprop_of non_triv_clauses)
    1.13  				val cnf_thm   = Thm.assume cnf_cterm
    1.14  				(* cf. Conjunction.elim_list *)
    1.15  				fun right_elim_list th =