changeset 36692 | 54b64d4ad524 |
parent 36614 | b6c031ad3690 |
child 36945 | 9bec62c10714 |
--- 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;