src/HOL/Library/refute.ML

       case t of
       (* Pure *)
         Const (@{const_name all}, _) => t
       | Const (@{const_name "=="}, _) => t
       | Const (@{const_name "==>"}, _) => t
-      | Const (@{const_name TYPE}, _) => t  (* axiomatic type classes *)
+      | Const (@{const_name Pure.type}, _) => t  (* axiomatic type classes *)
       (* HOL *)
       | Const (@{const_name Trueprop}, _) => t
       | Const (@{const_name Not}, _) => t
       | (* redundant, since 'True' is also an IDT constructor *)
         Const (@{const_name True}, _) => t

       (* Pure *)
         Const (@{const_name all}, _) => axs
       | Const (@{const_name "=="}, _) => axs
       | Const (@{const_name "==>"}, _) => axs
       (* axiomatic type classes *)
-      | Const (@{const_name TYPE}, T) => collect_type_axioms T axs
+      | Const (@{const_name Pure.type}, T) => collect_type_axioms T axs
       (* HOL *)
       | Const (@{const_name Trueprop}, _) => axs
       | Const (@{const_name Not}, _) => axs
       (* redundant, since 'True' is also an IDT constructor *)
       | Const (@{const_name True}, _) => axs