diff -r d95f39448121 -r 54b64d4ad524 src/HOL/Tools/cnf_funcs.ML
--- a/src/HOL/Tools/cnf_funcs.ML	Wed May 05 09:24:42 2010 +0200
+++ b/src/HOL/Tools/cnf_funcs.ML	Wed May 05 18:25:34 2010 +0200
@@ -122,7 +122,7 @@
 		  | dual x                      = HOLogic.Not $ x
 		(* Term.term list -> bool *)
 		fun has_duals []      = false
-		  | has_duals (x::xs) = (dual x) mem xs orelse has_duals xs
+		  | has_duals (x::xs) = member (op =) xs (dual x) orelse has_duals xs
 	in
 		has_duals (HOLogic.disjuncts c)
 	end;