changeset 20066 | b045b835cb3b |
parent 20039 | 4293f932fe83 |
child 20170 | 6ff853f82d73 |
--- a/src/HOL/Tools/sat_funcs.ML Sat Jul 08 14:12:13 2006 +0200 +++ b/src/HOL/Tools/sat_funcs.ML Mon Jul 10 21:02:29 2006 +0200 @@ -174,7 +174,7 @@ let val thy = theory_of_thm (if l1_is_neg then c2' else c1') val cP = cterm_of thy (Var (("P", 0), HOLogic.boolT)) - val cLit = (cterm_of thy o HOLogic.dest_Trueprop o term_of) (if l1_is_neg then l2 else l1) + val cLit = snd (Thm.dest_comb (if l1_is_neg then l2 else l1)) (* strip Trueprop *) in Thm.instantiate ([], [(cP, cLit)]) resolution_thm end