diff -r 636f84cd3639 -r b045b835cb3b src/HOL/Tools/sat_funcs.ML
--- 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