1.1 --- a/src/HOL/Tools/meson.ML	Tue Jul 11 12:16:57 2006 +0200
     1.2 +++ b/src/HOL/Tools/meson.ML	Tue Jul 11 12:16:58 2006 +0200
     1.3 @@ -122,7 +122,7 @@
     1.4    let val (poslits,neglits) = signed_lits th
     1.5    in  exists taut_poslit poslits
     1.6        orelse
     1.7 -      exists (fn t => mem_term (t, neglits)) (HOLogic.false_const :: poslits)
     1.8 +      exists (member (op aconv) neglits) (HOLogic.false_const :: poslits)
     1.9    end
    1.10    handle TERM _ => false;	(*probably dest_Trueprop on a weird theorem*)		      
    1.11