src/HOL/Library/Countable.thy

   fun countable_tac ctxt =
     SUBGOAL (fn (goal, i) =>
       let
         val ty_name =
           (case goal of
-            (_ $ Const (@{const_name TYPE}, Type (@{type_name itself}, [Type (n, _)]))) => n
+            (_ $ Const (@{const_name Pure.type}, Type (@{type_name itself}, [Type (n, _)]))) => n
           | _ => raise Match)
         val typedef_info = hd (Typedef.get_info ctxt ty_name)
         val typedef_thm = #type_definition (snd typedef_info)
         val pred_name =
           (case HOLogic.dest_Trueprop (concl_of typedef_thm) of