diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/HOL/Tools/inductive_realizer.ML
--- a/src/HOL/Tools/inductive_realizer.ML	Fri Mar 21 15:12:03 2014 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML	Fri Mar 21 20:33:56 2014 +0100
@@ -31,20 +31,21 @@
 
 val pred_of = fst o dest_Const o head_of;
 
-fun strip_all' used names (Const ("all", _) $ Abs (s, T, t)) =
+fun strip_all' used names (Const (@{const_name Pure.all}, _) $ Abs (s, T, t)) =
       let val (s', names') = (case names of
           [] => (singleton (Name.variant_list used) s, [])
         | name :: names' => (name, names'))
       in strip_all' (s'::used) names' (subst_bound (Free (s', T), t)) end
-  | strip_all' used names ((t as Const ("==>", _) $ P) $ Q) =
+  | strip_all' used names ((t as Const (@{const_name Pure.imp}, _) $ P) $ Q) =
       t $ strip_all' used names Q
   | strip_all' _ _ t = t;
 
 fun strip_all t = strip_all' (Term.add_free_names t []) [] t;
 
-fun strip_one name (Const ("all", _) $ Abs (s, T, Const ("==>", _) $ P $ Q)) =
+fun strip_one name
+    (Const (@{const_name Pure.all}, _) $ Abs (s, T, Const (@{const_name Pure.imp}, _) $ P $ Q)) =
       (subst_bound (Free (name, T), P), subst_bound (Free (name, T), Q))
-  | strip_one _ (Const ("==>", _) $ P $ Q) = (P, Q);
+  | strip_one _ (Const (@{const_name Pure.imp}, _) $ P $ Q) = (P, Q);
 
 fun relevant_vars prop = fold (fn ((a, i), T) => fn vs =>
      (case strip_type T of
@@ -145,8 +146,8 @@
 
     val is_rec = exists_Const (fn (c, _) => member (op =) rsets c);
 
-    fun is_meta (Const ("all", _) $ Abs (s, _, P)) = is_meta P
-      | is_meta (Const ("==>", _) $ _ $ Q) = is_meta Q
+    fun is_meta (Const (@{const_name Pure.all}, _) $ Abs (s, _, P)) = is_meta P
+      | is_meta (Const (@{const_name Pure.imp}, _) $ _ $ Q) = is_meta Q
       | is_meta (Const (@{const_name Trueprop}, _) $ t) =
           (case head_of t of
             Const (s, _) => can (Inductive.the_inductive ctxt) s