src/Pure/axclass.ML

     |> Sign.declare_const [] (c', T', NoSyn)
     |-> (fn const' as Const (c'', _) => Thm.add_def false true
           (Thm.def_name c', Logic.mk_equals (Const (c, T'), const'))
     #>> Thm.varifyT
     #-> (fn thm => add_inst_param (c, tyco) (c'', thm)
-    #> PureThy.note Thm.internalK (c', thm)
+    #> PureThy.add_thm ((c', thm), [PureThy.kind_internal])
     #> snd
     #> Sign.restore_naming thy
     #> pair (Const (c, T))))
   end;