src/HOL/Tools/cnf_funcs.ML
changeset 36692 54b64d4ad524
parent 36614 b6c031ad3690
child 36945 9bec62c10714
     1.1 --- a/src/HOL/Tools/cnf_funcs.ML	Wed May 05 09:24:42 2010 +0200
     1.2 +++ b/src/HOL/Tools/cnf_funcs.ML	Wed May 05 18:25:34 2010 +0200
     1.3 @@ -122,7 +122,7 @@
     1.4  		  | dual x                      = HOLogic.Not $ x
     1.5  		(* Term.term list -> bool *)
     1.6  		fun has_duals []      = false
     1.7 -		  | has_duals (x::xs) = (dual x) mem xs orelse has_duals xs
     1.8 +		  | has_duals (x::xs) = member (op =) xs (dual x) orelse has_duals xs
     1.9  	in
    1.10  		has_duals (HOLogic.disjuncts c)
    1.11  	end;