# HG changeset patch
# User wenzelm
# Date 1632219940 -7200
# Node ID bff865939cc3a5f0b31e8ad492d4573a1354cdd8
# Parent  534b231ce0413779499bd13a92e0c8e6ebf79e5c
clarified modules;

diff -r 534b231ce041 -r bff865939cc3 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Tue Sep 21 12:08:41 2021 +0200
+++ b/src/Pure/pure_thy.ML	Tue Sep 21 12:25:40 2021 +0200
@@ -29,18 +29,6 @@
 fun infixr_ (sy, p) = Infixr (Input.string sy, p, Position.no_range);
 fun binder (sy, p, q) = Binder (Input.string sy, p, q, Position.no_range);
 
-fun add_deps_type c thy =
-  let
-    val n = Sign.arity_number thy c;
-    val typargs = map (fn a => TFree (a, [])) (Name.invent Name.context Name.aT n);
-  in thy |> Theory.add_deps_global "" ((Defs.Type, c), typargs) [] end
-
-fun add_deps_const c thy =
-  let
-    val T = Logic.unvarifyT_global (Sign.the_const_type thy c);
-    val typargs = Sign.const_typargs thy (c, T);
-  in thy |> Theory.add_deps_global "" ((Defs.Const, c), typargs) [] end;
-
 
 (* application syntax variants *)
 
@@ -86,11 +74,11 @@
     (Binding.make ("itself", \<^here>), 1, NoSyn),
     (Binding.make ("dummy", \<^here>), 0, NoSyn),
     (qualify (Binding.make ("proof", \<^here>)), 0, NoSyn)]
-  #> add_deps_type "fun"
-  #> add_deps_type "prop"
-  #> add_deps_type "itself"
-  #> add_deps_type "dummy"
-  #> add_deps_type "Pure.proof"
+  #> Theory.add_deps_type "fun"
+  #> Theory.add_deps_type "prop"
+  #> Theory.add_deps_type "itself"
+  #> Theory.add_deps_type "dummy"
+  #> Theory.add_deps_type "Pure.proof"
   #> Sign.add_nonterminals_global
     (map (fn name => Binding.make (name, \<^here>))
       (Lexicon.terminals @ ["logic", "type", "types", "sort", "classes",
@@ -225,11 +213,11 @@
     (qualify (Binding.make ("Oracle", \<^here>)), typ "prop \<Rightarrow> Pure.proof", NoSyn),
     (qualify (Binding.make ("PClass", \<^here>)), typ "('a itself \<Rightarrow> prop) \<Rightarrow> Pure.proof", NoSyn),
     (qualify (Binding.make ("MinProof", \<^here>)), typ "Pure.proof", NoSyn)]
-  #> add_deps_const "Pure.eq"
-  #> add_deps_const "Pure.imp"
-  #> add_deps_const "Pure.all"
-  #> add_deps_const "Pure.type"
-  #> add_deps_const "Pure.dummy_pattern"
+  #> Theory.add_deps_const "Pure.eq"
+  #> Theory.add_deps_const "Pure.imp"
+  #> Theory.add_deps_const "Pure.all"
+  #> Theory.add_deps_const "Pure.type"
+  #> Theory.add_deps_const "Pure.dummy_pattern"
   #> Sign.parse_ast_translation Syntax_Trans.pure_parse_ast_translation
   #> Sign.parse_translation Syntax_Trans.pure_parse_translation
   #> Sign.print_ast_translation Syntax_Trans.pure_print_ast_translation
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;