src/Pure/primitive_defs.ML

     val (head, args) = Term.strip_comb lhs;
     val head_tfrees = Term.add_tfrees head [];
 
     fun check_arg (Bound _) = true
       | check_arg (Free (x, _)) = not (is_fixed x)
-      | check_arg (Const ("TYPE", Type ("itself", [TFree _]))) = true
+      | check_arg (Const ("Pure.type", Type ("itself", [TFree _]))) = true
       | check_arg _ = false;
     fun close_arg (Bound _) t = t
       | close_arg x t = Logic.all x t;
 
     val lhs_bads = filter_out check_arg args;