diff -r 534b231ce041 -r bff865939cc3 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Tue Sep 21 12:08:41 2021 +0200
+++ b/src/Pure/theory.ML	Tue Sep 21 12:25:40 2021 +0200
@@ -30,6 +30,8 @@
   val type_dep: string * typ list -> Defs.entry
   val add_deps: Defs.context -> string -> Defs.entry -> Defs.entry list -> theory -> theory
   val add_deps_global: string -> Defs.entry -> Defs.entry list -> theory -> theory
+  val add_deps_const: string -> theory -> theory
+  val add_deps_type: string -> theory -> theory
   val add_def: Defs.context -> bool -> bool -> binding * term -> theory -> theory
   val specify_const: (binding * typ) * mixfix -> theory -> term * theory
   val check_overloading: Proof.context -> bool -> string * typ -> unit
@@ -270,6 +272,16 @@
 fun add_deps_global a x y thy =
   add_deps (Defs.global_context thy) a x y thy;
 
+fun add_deps_const c thy =
+  let val T = Logic.unvarifyT_global (Sign.the_const_type thy c);
+  in thy |> add_deps_global "" (const_dep thy (c, T)) [] end;
+
+fun add_deps_type c thy =
+  let
+    val n = Sign.arity_number thy c;
+    val args = map (fn a => TFree (a, [])) (Name.invent Name.context Name.aT n);
+  in thy |> add_deps_global "" (type_dep (c, args)) [] end
+
 fun specify_const decl thy =
   let val (t, thy') = Sign.declare_const_global decl thy;
   in (t, add_deps_global "" (const_dep thy' (dest_Const t)) [] thy') end;