src/HOL/Tools/Meson/meson.ML

--- a/src/HOL/Tools/Meson/meson.ML	Fri Dec 02 14:37:25 2011 +0100
+++ b/src/HOL/Tools/Meson/meson.ML	Fri Dec 02 14:54:25 2011 +0100
@@ -231,7 +231,7 @@
   let val (poslits,neglits) = signed_lits th
   in  exists taut_poslit poslits
       orelse
-      exists (member (op aconv) neglits) (HOLogic.false_const :: poslits)
+      exists (member (op aconv) neglits) (@{term False} :: poslits)
   end
   handle TERM _ => false;       (*probably dest_Trueprop on a weird theorem*)