diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/HOL/Tools/Meson/meson_clausify.ML
--- a/src/HOL/Tools/Meson/meson_clausify.ML	Fri Mar 21 15:12:03 2014 +0100
+++ b/src/HOL/Tools/Meson/meson_clausify.ML	Fri Mar 21 20:33:56 2014 +0100
@@ -242,7 +242,7 @@
     fun aux (cluster as (cluster_no, cluster_skolem)) index_no pos t =
       case t of
         (t1 as Const (s, _)) $ Abs (s', T, t') =>
-        if s = @{const_name all} orelse s = @{const_name All} orelse
+        if s = @{const_name Pure.all} orelse s = @{const_name All} orelse
            s = @{const_name Ex} then
           let
             val skolem = (pos = (s = @{const_name Ex}))
@@ -254,7 +254,7 @@
         else
           t
       | (t1 as Const (s, _)) $ t2 $ t3 =>
-        if s = @{const_name "==>"} orelse s = @{const_name HOL.implies} then
+        if s = @{const_name Pure.imp} orelse s = @{const_name HOL.implies} then
           t1 $ aux cluster index_no (not pos) t2 $ aux cluster index_no pos t3
         else if s = @{const_name HOL.conj} orelse
                 s = @{const_name HOL.disj} then
@@ -275,13 +275,13 @@
   ct
   |> (case term_of ct of
         Const (s, _) $ Abs (s', _, _) =>
-        if s = @{const_name all} orelse s = @{const_name All} orelse
+        if s = @{const_name Pure.all} orelse s = @{const_name All} orelse
            s = @{const_name Ex} then
           Thm.dest_comb #> snd #> Thm.dest_abs (SOME s') #> snd #> zap pos
         else
           Conv.all_conv
       | Const (s, _) $ _ $ _ =>
-        if s = @{const_name "==>"} orelse s = @{const_name implies} then
+        if s = @{const_name Pure.imp} orelse s = @{const_name implies} then
           Conv.combination_conv (Conv.arg_conv (zap (not pos))) (zap pos)
         else if s = @{const_name conj} orelse s = @{const_name disj} then
           Conv.combination_conv (Conv.arg_conv (zap pos)) (zap pos)