# HG changeset patch
# User wenzelm
# Date 1632220538 -7200
# Node ID e098fa45bfe037ef75185526f7f72f93d08a0593
# Parent  bff865939cc3a5f0b31e8ad492d4573a1354cdd8
proper Sign.const_typargs via Theory.add_deps_const/Theory.const_dep;

diff -r bff865939cc3 -r e098fa45bfe0 src/Pure/Isar/object_logic.ML
--- 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))