--- 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))