src/HOL/Tools/Meson/meson.ML
changeset 45740 132a3e1c0fe5
parent 45567 8e3891309a8e
child 45981 4c629115e3ab
     1.1 --- a/src/HOL/Tools/Meson/meson.ML	Fri Dec 02 14:37:25 2011 +0100
     1.2 +++ b/src/HOL/Tools/Meson/meson.ML	Fri Dec 02 14:54:25 2011 +0100
     1.3 @@ -231,7 +231,7 @@
     1.4    let val (poslits,neglits) = signed_lits th
     1.5    in  exists taut_poslit poslits
     1.6        orelse
     1.7 -      exists (member (op aconv) neglits) (HOLogic.false_const :: poslits)
     1.8 +      exists (member (op aconv) neglits) (@{term False} :: poslits)
     1.9    end
    1.10    handle TERM _ => false;       (*probably dest_Trueprop on a weird theorem*)
    1.11