src/HOL/Tools/record.ML

 fun split_simproc P =
   Simplifier.simproc_global @{theory HOL} "record_split_simp" ["x"]
     (fn ctxt => fn t =>
       (case t of
         Const (quantifier, Type (_, [Type (_, [T, _]), _])) $ _ =>
-          if quantifier = @{const_name all} orelse
+          if quantifier = @{const_name Pure.all} orelse
             quantifier = @{const_name All} orelse
             quantifier = @{const_name Ex}
           then
             (case rec_id ~1 T of
               "" => NONE

                     (case get_splits (Proof_Context.theory_of ctxt) (rec_id split T) of
                       NONE => NONE
                     | SOME (all_thm, All_thm, Ex_thm, _) =>
                         SOME
                           (case quantifier of
-                            @{const_name all} => all_thm
+                            @{const_name Pure.all} => all_thm
                           | @{const_name All} => All_thm RS @{thm eq_reflection}
                           | @{const_name Ex} => Ex_thm RS @{thm eq_reflection}
                           | _ => raise Fail "split_simproc"))
                   else NONE
                 end)

     val goal = term_of cgoal;
     val frees = filter (is_recT o #2) (Term.add_frees goal []);
 
     val has_rec = exists_Const
       (fn (s, Type (_, [Type (_, [T, _]), _])) =>
-          (s = @{const_name all} orelse s = @{const_name All} orelse s = @{const_name Ex}) andalso
-          is_recT T
+          (s = @{const_name Pure.all} orelse s = @{const_name All} orelse s = @{const_name Ex})
+            andalso is_recT T
         | _ => false);
 
     fun mk_split_free_tac free induct_thm i =
       let
         val cfree = cterm_of thy free;

   let
     val goal = term_of cgoal;
 
     val has_rec = exists_Const
       (fn (s, Type (_, [Type (_, [T, _]), _])) =>
-          (s = @{const_name all} orelse s = @{const_name All}) andalso is_recT T
+          (s = @{const_name Pure.all} orelse s = @{const_name All}) andalso is_recT T
         | _ => false);
 
-    fun is_all (Const (@{const_name all}, _) $ _) = ~1
+    fun is_all (Const (@{const_name Pure.all}, _) $ _) = ~1
       | is_all (Const (@{const_name All}, _) $ _) = ~1
       | is_all _ = 0;
   in
     if has_rec goal then
       full_simp_tac (put_simpset HOL_basic_ss ctxt addsimprocs [split_simproc is_all]) i