src/HOL/Tools/inductive_realizer.ML

       let val ys = subsets xs
       in ys @ map (cons x) ys end;
 
 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
         (_, Type (s, _)) => if s = @{type_name bool} then (a, T) :: vs else vs
       | _ => vs)) (Term.add_vars prop []) [];

     val conclT = Extraction.etype_of thy vs [] (Logic.strip_imp_concl rule');
     val used = map (fst o dest_Free) args;
 
     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
           | _ => true)
       | is_meta _ = false;