proper Sign.const_typargs via Theory.add_deps_const/Theory.const_dep;

--- a/src/Pure/Isar/object_logic.ML	Tue Sep 21 12:25:40 2021 +0200
+++ b/src/Pure/Isar/object_logic.ML	Tue Sep 21 12:35:38 2021 +0200
@@ -91,10 +91,9 @@
   let
     val c = Sign.full_name thy b;
     val thy' = thy |> add_consts [(b, T, mx)];
-    val T' = Logic.unvarifyT_global (Sign.the_const_type thy' c);
   in
     thy'
-    |> Theory.add_deps_global "" (Theory.const_dep thy' (c, T')) []
+    |> Theory.add_deps_const c
     |> (Context.theory_map o map_data) (fn (base_sort, judgment, atomize_rulify) =>
         if is_some judgment then error "Attempt to redeclare object-logic judgment"
         else (base_sort, SOME c, atomize_rulify))