src/Pure/axclass.ML

   end;
 
 fun class_const c =
   (Logic.const_of_class c, Term.itselfT (Term.aT []) --> propT);
 
+fun class_const_dep c =
+  ((Defs.Constant, Logic.const_of_class c), [Term.aT []]);
+
 in
 
 val classrel_axiomatization =
   add_axioms (map o cert_classrel) (map Logic.mk_classrel)
     (map (prefix classrel_prefix o Logic.name_classrel)) add_classrel;

     val super = map (Sign.certify_class thy) raw_super |> Sign.minimize_sort thy;
   in
     thy
     |> Sign.primitive_class (bclass, super)
     |> classrel_axiomatization (map (fn c => (class, c)) super)
-    |> Theory.add_deps_global "" (Theory.DConst (class_const class))
-      (map (Theory.DConst o class_const) super)
+    |> Theory.add_deps_global "" (class_const_dep class) (map class_const_dep super)
   end;
 
 end;
 
 end;