HOL typedef with explicit dependency checks according to Ondrey Kuncar, 07-Jul-2015, 16-Jul-2015, 30-Jul-2015;
defs.ML: track dependencies also for type constructors;
typedef.ML: add type defined by typedef to dependencies, Abs and Rep now depend on the type;
Pure types and typedecls are final -- no dependencies;

--- a/src/Doc/Implementation/Logic.thy	Tue Sep 22 08:38:25 2015 +0200
+++ b/src/Doc/Implementation/Logic.thy	Tue Sep 22 14:32:23 2015 +0200
@@ -667,7 +667,7 @@
   \end{mldecls}
   \begin{mldecls}
   @{index_ML Theory.add_deps: "Proof.context -> string ->
-  string * typ -> (string * typ) list -> theory -> theory"} \\
+  Theory.dep -> Theory.dep list -> theory -> theory"} \\
   \end{mldecls}
 
   \begin{description}

--- a/src/HOL/Library/bnf_axiomatization.ML	Tue Sep 22 08:38:25 2015 +0200
+++ b/src/HOL/Library/bnf_axiomatization.ML	Tue Sep 22 14:32:23 2015 +0200
@@ -35,9 +35,9 @@
     fun mk_b name user_b =
       (if Binding.is_empty user_b then Binding.prefix_name (name ^ "_") b else user_b)
       |> Binding.qualify false (Binding.name_of b);
-    val (Tname, lthy) = Typedecl.basic_typedecl (b, length vars, mx) lthy;
+    val (Tname, lthy) = Typedecl.basic_typedecl true (b, length vars, mx) lthy;
     val (bd_type_Tname, lthy) =
-      Typedecl.basic_typedecl (mk_b "bd_type" Binding.empty, length deads, NoSyn) lthy;
+      Typedecl.basic_typedecl true (mk_b "bd_type" Binding.empty, length deads, NoSyn) lthy;
     val T = Type (Tname, map TFree vars);
     val bd_type_T = Type (bd_type_Tname, map TFree deads);
     val lives = map TFree (filter_out (member (op =) deads) vars);

--- a/src/HOL/SPARK/Tools/spark_vcs.ML	Tue Sep 22 08:38:25 2015 +0200
+++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Tue Sep 22 14:32:23 2015 +0200
@@ -389,7 +389,7 @@
        case get_type thy prfx s of
          SOME _ => thy
        | NONE => Typedecl.typedecl_global
-           (Binding.name s, [], NoSyn) thy |> snd);
+           true (Binding.name s, [], NoSyn) thy |> snd);
 
 
 fun term_of_expr thy prfx types pfuns =

--- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Tue Sep 22 08:38:25 2015 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Tue Sep 22 14:32:23 2015 +0200
@@ -199,7 +199,7 @@
       val tyargs =
         List.tabulate (arity, rpair @{sort type} o prefix "'" o string_of_int)
       val thy' =
-        Typedecl.typedecl_global (mk_binding config type_name, tyargs, NoSyn) thy
+        Typedecl.typedecl_global true (mk_binding config type_name, tyargs, NoSyn) thy
         |> snd
       val typ_map_entry = (thf_type, (final_fqn, arity))
       val ty_map' = typ_map_entry :: ty_map

--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Sep 22 08:38:25 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Sep 22 14:32:23 2015 +0200
@@ -1923,7 +1923,7 @@
       ||>> variant_tfrees fp_b_names;
 
     fun add_fake_type spec =
-      Typedecl.basic_typedecl (type_binding_of_spec spec, num_As, mixfix_of_spec spec);
+      Typedecl.basic_typedecl true (type_binding_of_spec spec, num_As, mixfix_of_spec spec);
 
     val (fake_T_names, fake_lthy) = fold_map add_fake_type specs no_defs_lthy;
 

--- a/src/HOL/Tools/typedef.ML	Tue Sep 22 08:38:25 2015 +0200
+++ b/src/HOL/Tools/typedef.ML	Tue Sep 22 14:32:23 2015 +0200
@@ -132,14 +132,22 @@
       |> Local_Theory.background_theory_result
         (Sign.declare_const lthy ((Rep_name, newT --> oldT), NoSyn) ##>>
           Sign.declare_const lthy ((Abs_name, oldT --> newT), NoSyn));
-
-    val typedef_deps = Term.add_consts A [];
+       
+    fun fold_type_constr f (Type (name, Ts)) = f (name,Ts) #> fold (fold_type_constr f) Ts
+      | fold_type_constr _ _ = I;
+    
+    val A_consts = fold_aterms (fn Const const => insert (op =) (Theory.DConst const) | _ => I) A [];
+    val A_types = fold_types (fold_type_constr (insert (op =) o Theory.DType)) A []
+    val typedef_deps = A_consts @ A_types;
+    
+    val newT_dep = Theory.DType (dest_Type newT);
 
     val ((axiom_name, axiom), axiom_lthy) = consts_lthy
       |> Local_Theory.background_theory_result
         (Thm.add_axiom consts_lthy (type_definition_name, mk_typedef newT oldT RepC AbsC A) ##>
-          Theory.add_deps consts_lthy "" (dest_Const RepC) typedef_deps ##>
-          Theory.add_deps consts_lthy "" (dest_Const AbsC) typedef_deps);
+          Theory.add_deps consts_lthy "" newT_dep typedef_deps ##>
+          Theory.add_deps consts_lthy "" (Theory.DConst (dest_Const RepC)) [newT_dep] ##>
+          Theory.add_deps consts_lthy "" (Theory.DConst (dest_Const AbsC)) [newT_dep]);
 
   in ((RepC, AbsC, axiom_name, axiom), axiom_lthy) end;
 
@@ -187,7 +195,7 @@
 
     val args = map (Proof_Context.check_tfree tmp_ctxt') raw_args;
     val (newT, typedecl_lthy) = lthy
-      |> Typedecl.typedecl (name, args, mx)
+      |> Typedecl.typedecl false (name, args, mx)
       ||> Variable.declare_term set;
 
     val Type (full_name, _) = newT;

--- a/src/Pure/Isar/isar_syn.ML	Tue Sep 22 08:38:25 2015 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Tue Sep 22 14:32:23 2015 +0200
@@ -22,7 +22,7 @@
 val _ =
   Outer_Syntax.local_theory @{command_keyword typedecl} "type declaration"
     (Parse.type_args -- Parse.binding -- Parse.opt_mixfix
-      >> (fn ((args, a), mx) => Typedecl.typedecl (a, map (rpair dummyS) args, mx) #> snd));
+      >> (fn ((args, a), mx) => Typedecl.typedecl true (a, map (rpair dummyS) args, mx) #> snd));
 
 val _ =
   Outer_Syntax.local_theory @{command_keyword type_synonym} "declare type abbreviation"

--- a/src/Pure/Isar/object_logic.ML	Tue Sep 22 08:38:25 2015 +0200
+++ b/src/Pure/Isar/object_logic.ML	Tue Sep 22 14:32:23 2015 +0200
@@ -90,7 +90,7 @@
   let val c = Sign.full_name thy b in
     thy
     |> add_consts [(b, T, mx)]
-    |> (fn thy' => Theory.add_deps_global c (c, Sign.the_const_type thy' c) [] thy')
+    |> (fn thy' => Theory.add_deps_global c (Theory.DConst (c, Sign.the_const_type thy' c)) [] thy')
     |> (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))

--- a/src/Pure/Isar/typedecl.ML	Tue Sep 22 08:38:25 2015 +0200
+++ b/src/Pure/Isar/typedecl.ML	Tue Sep 22 14:32:23 2015 +0200
@@ -7,9 +7,9 @@
 signature TYPEDECL =
 sig
   val read_constraint: Proof.context -> string option -> sort
-  val basic_typedecl: binding * int * mixfix -> local_theory -> string * local_theory
-  val typedecl: binding * (string * sort) list * mixfix -> local_theory -> typ * local_theory
-  val typedecl_global: binding * (string * sort) list * mixfix -> theory -> typ * theory
+  val basic_typedecl: bool -> binding * int * mixfix -> local_theory -> string * local_theory
+  val typedecl: bool -> binding * (string * sort) list * mixfix -> local_theory -> typ * local_theory
+  val typedecl_global: bool -> binding * (string * sort) list * mixfix -> theory -> typ * theory
   val abbrev: binding * string list * mixfix -> typ -> local_theory -> string * local_theory
   val abbrev_cmd: binding * string list * mixfix -> string -> local_theory -> string * local_theory
   val abbrev_global: binding * string list * mixfix -> typ -> theory -> string * theory
@@ -35,13 +35,6 @@
     |> pair name
   end;
 
-fun basic_typedecl (b, n, mx) lthy =
-  basic_decl (fn name =>
-    Sign.add_type lthy (b, n, NoSyn) #>
-    (case Object_Logic.get_base_sort lthy of
-      SOME S => Axclass.arity_axiomatization (name, replicate n S, S)
-    | NONE => I)) (b, n, mx) lthy;
-
 
 (* global type -- without dependencies on type parameters of the context *)
 
@@ -61,21 +54,41 @@
         commas_quote (map (Syntax.string_of_typ lthy) bad_args));
   in T end;
 
+fun basic_typedecl final (b, n, mx) lthy =
+  let
+    fun make_final lthy = 
+      let
+        val tfree_names = Name.invent (Variable.names_of lthy) Name.aT n
+        val tfrees = map (fn name => (name, [])) tfree_names
+        val T = global_type lthy (b, tfrees)
+      in
+        Local_Theory.background_theory (Theory.add_deps lthy "" (Theory.DType (dest_Type T)) []) lthy
+      end
+  in
+    lthy
+    |> basic_decl (fn name =>
+      Sign.add_type lthy (b, n, NoSyn) #>
+      (case Object_Logic.get_base_sort lthy of
+        SOME S => Axclass.arity_axiomatization (name, replicate n S, S)
+      | NONE => I)) (b, n, mx)
+    ||> (if final then make_final else I)
+  end
+
 
 (* type declarations *)
 
-fun typedecl (b, raw_args, mx) lthy =
+fun typedecl final (b, raw_args, mx) lthy =
   let val T = global_type lthy (b, raw_args) in
     lthy
-    |> basic_typedecl (b, length raw_args, mx)
+    |> basic_typedecl final (b, length raw_args, mx)
     |> snd
     |> Variable.declare_typ T
     |> pair T
   end;
 
-fun typedecl_global decl =
+fun typedecl_global final decl =
   Named_Target.theory_init
-  #> typedecl decl
+  #> typedecl final decl
   #> Local_Theory.exit_result_global Morphism.typ;
 
 

--- a/src/Pure/axclass.ML	Tue Sep 22 08:38:25 2015 +0200
+++ b/src/Pure/axclass.ML	Tue Sep 22 14:32:23 2015 +0200
@@ -614,7 +614,8 @@
     thy
     |> Sign.primitive_class (bclass, super)
     |> classrel_axiomatization (map (fn c => (class, c)) super)
-    |> Theory.add_deps_global "" (class_const class) (map class_const super)
+    |> Theory.add_deps_global "" (Theory.DConst (class_const class)) 
+      (map (Theory.DConst o class_const) super)
   end;
 
 end;

--- a/src/Pure/defs.ML	Tue Sep 22 08:38:25 2015 +0200
+++ b/src/Pure/defs.ML	Tue Sep 22 14:32:23 2015 +0200
@@ -7,7 +7,9 @@
 
 signature DEFS =
 sig
-  val pretty_const: Proof.context -> string * typ list -> Pretty.T
+  datatype node = NConst of string | NType of string
+  val fast_node_ord: node * node -> order
+  val pretty_node: Proof.context -> node * typ list -> Pretty.T
   val plain_args: typ list -> bool
   type T
   type spec =
@@ -15,31 +17,44 @@
     description: string,
     pos: Position.T,
     lhs: typ list,
-    rhs: (string * typ list) list}
-  val all_specifications_of: T -> (string * spec list) list
-  val specifications_of: T -> string -> spec list
+    rhs: (node * typ list) list}
+  val all_specifications_of: T -> (node * spec list) list
+  val specifications_of: T -> node -> spec list
   val dest: T ->
-   {restricts: ((string * typ list) * string) list,
-    reducts: ((string * typ list) * (string * typ list) list) list}
+   {restricts: ((node * typ list) * string) list,
+    reducts: ((node * typ list) * (node * typ list) list) list}
   val empty: T
   val merge: Proof.context -> T * T -> T
   val define: Proof.context -> bool -> string option -> string ->
-    string * typ list -> (string * typ list) list -> T -> T
+    node * typ list -> (node * typ list) list -> T -> T
 end
 
+
 structure Defs: DEFS =
 struct
 
+datatype node = NConst of string | NType of string
+
+fun fast_node_ord (NConst s1, NConst s2) = fast_string_ord (s1, s2)
+  | fast_node_ord (NType s1, NType s2) = fast_string_ord (s1, s2)
+  | fast_node_ord (NConst _, NType _) = LESS
+  | fast_node_ord (NType _, NConst _) = GREATER
+
+fun string_of_node (NConst s) = "constant " ^ s
+  | string_of_node (NType s) = "type " ^ s
+
+structure Deftab = Table(type key = node val ord = fast_node_ord);
+
 (* type arguments *)
 
 type args = typ list;
 
-fun pretty_const ctxt (c, args) =
+fun pretty_node ctxt (c, args) =
   let
     val prt_args =
       if null args then []
       else [Pretty.list "(" ")" (map (Syntax.pretty_typ ctxt o Logic.unvarifyT_global) args)];
-  in Pretty.block (Pretty.str c :: prt_args) end;
+  in Pretty.block (Pretty.str (string_of_node c) :: prt_args) end;
 
 fun plain_args args =
   forall Term.is_TVar args andalso not (has_duplicates (op =) args);
@@ -63,31 +78,31 @@
   description: string,
   pos: Position.T,
   lhs: args,
-  rhs: (string * args) list};
+  rhs: (node * args) list};
 
 type def =
  {specs: spec Inttab.table,  (*source specifications*)
   restricts: (args * string) list,  (*global restrictions imposed by incomplete patterns*)
-  reducts: (args * (string * args) list) list};  (*specifications as reduction system*)
+  reducts: (args * (node * args) list) list};  (*specifications as reduction system*)
 
 fun make_def (specs, restricts, reducts) =
   {specs = specs, restricts = restricts, reducts = reducts}: def;
 
 fun map_def c f =
-  Symtab.default (c, make_def (Inttab.empty, [], [])) #>
-  Symtab.map_entry c (fn {specs, restricts, reducts}: def =>
+  Deftab.default (c, make_def (Inttab.empty, [], [])) #>
+  Deftab.map_entry c (fn {specs, restricts, reducts}: def =>
     make_def (f (specs, restricts, reducts)));
 
 
-datatype T = Defs of def Symtab.table;
+datatype T = Defs of def Deftab.table;
 
 fun lookup_list which defs c =
-  (case Symtab.lookup defs c of
+  (case Deftab.lookup defs c of
     SOME (def: def) => which def
   | NONE => []);
 
 fun all_specifications_of (Defs defs) =
-  (map o apsnd) (map snd o Inttab.dest o #specs) (Symtab.dest defs);
+  (map o apsnd) (map snd o Inttab.dest o #specs) (Deftab.dest defs);
 
 fun specifications_of (Defs defs) = lookup_list (map snd o Inttab.dest o #specs) defs;
 
@@ -96,13 +111,13 @@
 
 fun dest (Defs defs) =
   let
-    val restricts = Symtab.fold (fn (c, {restricts, ...}) =>
+    val restricts = Deftab.fold (fn (c, {restricts, ...}) =>
       fold (fn (args, description) => cons ((c, args), description)) restricts) defs [];
-    val reducts = Symtab.fold (fn (c, {reducts, ...}) =>
+    val reducts = Deftab.fold (fn (c, {reducts, ...}) =>
       fold (fn (args, deps) => cons ((c, args), deps)) reducts) defs [];
   in {restricts = restricts, reducts = reducts} end;
 
-val empty = Defs Symtab.empty;
+val empty = Defs Deftab.empty;
 
 
 (* specifications *)
@@ -110,7 +125,7 @@
 fun disjoint_specs c (i, {description = a, pos = pos_a, lhs = Ts, ...}: spec) =
   Inttab.forall (fn (j, {description = b, pos = pos_b, lhs = Us, ...}: spec) =>
     i = j orelse disjoint_args (Ts, Us) orelse
-      error ("Clash of specifications for constant " ^ quote c ^ ":\n" ^
+      error ("Clash of specifications for " ^ quote (string_of_node c) ^ ":\n" ^
         "  " ^ quote a ^ Position.here pos_a ^ "\n" ^
         "  " ^ quote b ^ Position.here pos_b));
 
@@ -128,9 +143,9 @@
 
 local
 
-val prt = Pretty.string_of oo pretty_const;
+val prt = Pretty.string_of oo pretty_node;
 fun err ctxt (c, args) (d, Us) s1 s2 =
-  error (s1 ^ " dependency of constant " ^ prt ctxt (c, args) ^ " -> " ^ prt ctxt (d, Us) ^ s2);
+  error (s1 ^ " dependency of " ^ prt ctxt (c, args) ^ " -> " ^ prt ctxt (d, Us) ^ s2);
 
 fun acyclic ctxt (c, args) (d, Us) =
   c <> d orelse
@@ -174,12 +189,12 @@
         else (true, defs |> map_def c (fn (specs, restricts, _) => (specs, restricts, reducts')))
       end;
     fun norm_all defs =
-      (case Symtab.fold norm_update defs (false, defs) of
+      (case Deftab.fold norm_update defs (false, defs) of
         (true, defs') => norm_all defs'
       | (false, _) => defs);
     fun check defs (c, {reducts, ...}: def) =
       reducts |> forall (fn (args, deps) => forall (wellformed ctxt defs (c, args)) deps);
-  in norm_all #> (fn defs => tap (Symtab.forall (check defs)) defs) end;
+  in norm_all #> (fn defs => tap (Deftab.forall (check defs)) defs) end;
 
 fun dependencies ctxt (c, args) restr deps =
   map_def c (fn (specs, restricts, reducts) =>
@@ -202,8 +217,8 @@
     fun add_def (c, {restricts, reducts, ...}: def) =
       fold (fn (args, deps) => add_deps (c, args) restricts deps) reducts;
   in
-    Defs (Symtab.join join_specs (defs1, defs2)
-      |> normalize ctxt |> Symtab.fold add_def defs2)
+    Defs (Deftab.join join_specs (defs1, defs2)
+      |> normalize ctxt |> Deftab.fold add_def defs2)
   end;
 
 

--- a/src/Pure/display.ML	Tue Sep 22 08:38:25 2015 +0200
+++ b/src/Pure/display.ML	Tue Sep 22 14:32:23 2015 +0200
@@ -104,7 +104,8 @@
     fun prt_term t = Pretty.quote (Syntax.pretty_term ctxt t);
     val prt_term_no_vars = prt_term o Logic.unvarify_global;
     fun prt_const (c, ty) = [Pretty.mark_str c, Pretty.str " ::", Pretty.brk 1, prt_typ_no_tvars ty];
-    val prt_const' = Defs.pretty_const ctxt;
+    val prt_node = Defs.pretty_node ctxt;
+    fun sort_node_wrt f = sort (Defs.fast_node_ord o apply2 f)
 
     fun pretty_classrel (c, []) = prt_cls c
       | pretty_classrel (c, cs) = Pretty.block
@@ -134,26 +135,29 @@
       Pretty.block [Pretty.mark_str a, Pretty.str ":", Pretty.brk 1, prt_term_no_vars t];
 
     fun pretty_finals reds = Pretty.block
-      (Pretty.str "final:" :: Pretty.brk 1 :: Pretty.commas (map (prt_const' o fst) reds));
+      (Pretty.str "final:" :: Pretty.brk 1 :: Pretty.commas (map (prt_node o fst) reds));
 
     fun pretty_reduct (lhs, rhs) = Pretty.block
-      ([prt_const' lhs, Pretty.str "  ->", Pretty.brk 2] @
-        Pretty.commas (map prt_const' (sort_by #1 rhs)));
+      ([prt_node lhs, Pretty.str "  ->", Pretty.brk 2] @
+        Pretty.commas (map prt_node ((sort_node_wrt #1) rhs)));
 
     fun pretty_restrict (const, name) =
-      Pretty.block ([prt_const' const, Pretty.brk 2, Pretty.str ("(from " ^ quote name ^ ")")]);
+      Pretty.block ([prt_node const, Pretty.brk 2, Pretty.str ("(from " ^ quote name ^ ")")]);
 
     val defs = Theory.defs_of thy;
     val {restricts, reducts} = Defs.dest defs;
     val tsig = Sign.tsig_of thy;
     val consts = Sign.consts_of thy;
     val {const_space, constants, constraints} = Consts.dest consts;
-    val extern_const = Name_Space.extern ctxt const_space;
     val {classes, default, types, ...} = Type.rep_tsig tsig;
+    val type_space = Type.type_space tsig;
     val (class_space, class_algebra) = classes;
     val classes = Sorts.classes_of class_algebra;
     val arities = Sorts.arities_of class_algebra;
 
+    fun extern_node (Defs.NConst c) = Defs.NConst (Name_Space.extern ctxt const_space c)
+      | extern_node (Defs.NType t) = Defs.NType (Name_Space.extern ctxt type_space t);
+
     val clsses =
       Name_Space.extern_entries verbose ctxt class_space
         (map (fn ((c, _), cs) => (c, Sign.minimize_sort thy cs)) (Graph.dest classes))
@@ -163,6 +167,11 @@
       Name_Space.extern_entries verbose ctxt (Type.type_space tsig) (Symtab.dest arities)
       |> map (apfst #1);
 
+    fun prune_const c = not verbose andalso Consts.is_concealed consts c;
+
+    fun prune_node (Defs.NConst c) = prune_const c
+      | prune_node (Defs.NType t) = not verbose andalso Name_Space.is_concealed type_space t;
+
     val cnsts = Name_Space.markup_entries verbose ctxt const_space constants;
     val log_cnsts = map_filter (fn (c, (ty, NONE)) => SOME (c, ty) | _ => NONE) cnsts;
     val abbrevs = map_filter (fn (c, (ty, SOME t)) => SOME (c, (ty, t)) | _ => NONE) cnsts;
@@ -170,14 +179,13 @@
 
     val axms = Name_Space.markup_table verbose ctxt (Theory.axiom_table thy);
 
-    fun prune_const c = not verbose andalso Consts.is_concealed consts c;
-    val (reds0, (reds1, reds2)) = filter_out (prune_const o fst o fst) reducts
+    val (reds0, (reds1, reds2)) = filter_out (prune_node o fst o fst) reducts
       |> map (fn (lhs, rhs) =>
-        (apfst extern_const lhs, map (apfst extern_const) (filter_out (prune_const o fst) rhs)))
-      |> sort_by (#1 o #1)
+        (apfst extern_node lhs, map (apfst extern_node) (filter_out (prune_node o fst) rhs)))
+      |> sort_node_wrt (#1 o #1)
       |> List.partition (null o #2)
       ||> List.partition (Defs.plain_args o #2 o #1);
-    val rests = restricts |> map (apfst (apfst extern_const)) |> sort_by (#1 o #1);
+    val rests = restricts |> map (apfst (apfst extern_node)) |> sort_node_wrt (#1 o #1);
   in
     [Pretty.strs ("names:" :: Context.display_names thy)] @
     [Pretty.big_list "classes:" (map pretty_classrel clsses),

--- a/src/Pure/pure_thy.ML	Tue Sep 22 08:38:25 2015 +0200
+++ b/src/Pure/pure_thy.ML	Tue Sep 22 14:32:23 2015 +0200
@@ -66,6 +66,10 @@
     (Binding.make ("prop", @{here}), 0, NoSyn),
     (Binding.make ("itself", @{here}), 1, NoSyn),
     (Binding.make ("dummy", @{here}), 0, NoSyn)]
+  #> Theory.add_deps_global "fun" (Theory.DType ("fun", [typ "'a", typ "'b"])) []
+  #> Theory.add_deps_global "prop" (Theory.DType ("prop", [])) []
+  #> Theory.add_deps_global "itself" (Theory.DType ("itself", [typ "'a"])) []
+  #> Theory.add_deps_global "dummy" (Theory.DType ("dummy", [])) []
   #> Sign.add_nonterminals_global
     (map (fn name => Binding.make (name, @{here}))
       (Lexicon.terminals @ ["logic", "type", "types", "sort", "classes",
@@ -194,11 +198,11 @@
     (qualify (Binding.make ("prop", @{here})), typ "prop => prop", NoSyn),
     (qualify (Binding.make ("type", @{here})), typ "'a itself", NoSyn),
     (qualify (Binding.make ("dummy_pattern", @{here})), typ "'a", Delimfix "'_")]
-  #> Theory.add_deps_global "Pure.eq" ("Pure.eq", typ "'a => 'a => prop") []
-  #> Theory.add_deps_global "Pure.imp" ("Pure.imp", typ "prop => prop => prop") []
-  #> Theory.add_deps_global "Pure.all" ("Pure.all", typ "('a => prop) => prop") []
-  #> Theory.add_deps_global "Pure.type" ("Pure.type", typ "'a itself") []
-  #> Theory.add_deps_global "Pure.dummy_pattern" ("Pure.dummy_pattern", typ "'a") []
+  #> Theory.add_deps_global "Pure.eq" (Theory.DConst ("Pure.eq", typ "'a => 'a => prop")) []
+  #> Theory.add_deps_global "Pure.imp" (Theory.DConst ("Pure.imp", typ "prop => prop => prop")) []
+  #> Theory.add_deps_global "Pure.all" (Theory.DConst ("Pure.all", typ "('a => prop) => prop")) []
+  #> Theory.add_deps_global "Pure.type" (Theory.DConst ("Pure.type", typ "'a itself")) []
+  #> Theory.add_deps_global "Pure.dummy_pattern" (Theory.DConst ("Pure.dummy_pattern", typ "'a")) []
   #> 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

--- a/src/Pure/theory.ML	Tue Sep 22 08:38:25 2015 +0200
+++ b/src/Pure/theory.ML	Tue Sep 22 14:32:23 2015 +0200
@@ -23,8 +23,9 @@
   val begin_theory: string * Position.T -> theory list -> theory
   val end_theory: theory -> theory
   val add_axiom: Proof.context -> binding * term -> theory -> theory
-  val add_deps: Proof.context -> string -> string * typ -> (string * typ) list -> theory -> theory
-  val add_deps_global: string -> string * typ -> (string * typ) list -> theory -> theory
+  datatype dep = DConst of string * typ | DType of string * typ list 
+  val add_deps: Proof.context -> string -> dep -> dep list -> theory -> theory
+  val add_deps_global: string -> dep -> dep list -> theory -> theory
   val add_def: Proof.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
@@ -211,17 +212,26 @@
 
 (* dependencies *)
 
+datatype dep = DConst of string * typ | DType of string * typ list 
+
+fun name_of_dep (DConst (s, _)) = s
+  | name_of_dep (DType (s, _)) = s
+
 fun dependencies ctxt unchecked def description lhs rhs =
   let
     val thy = Proof_Context.theory_of ctxt;
     val consts = Sign.consts_of thy;
-    fun prep const =
+    fun prep (DConst const) =
       let val Const (c, T) = Sign.no_vars ctxt (Const const)
-      in (c, Consts.typargs consts (c, Logic.varifyT_global T)) end;
-
-    val lhs_vars = Term.add_tfreesT (#2 lhs) [];
-    val rhs_extras = fold (#2 #> Term.fold_atyps (fn TFree v =>
-      if member (op =) lhs_vars v then I else insert (op =) v | _ => I)) rhs [];
+      in (Defs.NConst c, Consts.typargs consts (c, Logic.varifyT_global T)) end
+    | prep (DType typ) = 
+      let val Type (c, T) = Type.no_tvars (Type typ)
+      in (Defs.NType c, map Logic.varifyT_global T) end;
+    fun fold_dep_tfree f (DConst (_, T)) = fold_atyps (fn TFree v => f v | _ => I) T
+      | fold_dep_tfree f (DType (_, Ts)) = fold (fold_atyps (fn TFree v => f v | _ => I)) Ts
+    val lhs_vars = fold_dep_tfree (insert (op =)) lhs [];
+    val rhs_extras = fold (fold_dep_tfree 
+      (fn v => if member (op =) lhs_vars v then I else insert (op =) v)) rhs [];
     val _ =
       if null rhs_extras then ()
       else error ("Specification depends on extra type variables: " ^
@@ -231,15 +241,17 @@
 
 fun add_deps ctxt a raw_lhs raw_rhs thy =
   let
-    val lhs :: rhs = map (dest_Const o Sign.cert_term thy o Const) (raw_lhs :: raw_rhs);
-    val description = if a = "" then #1 lhs ^ " axiom" else a;
+    fun cert_dep (DConst const) = const |> Const |> Sign.cert_term thy |> dest_Const |> DConst
+      | cert_dep (DType typ) = typ |> Type |> Sign.certify_typ thy |> dest_Type |> DType;
+    val lhs :: rhs = map cert_dep (raw_lhs :: raw_rhs);
+    val description = if a = "" then name_of_dep lhs ^ " axiom" else a;
   in thy |> map_defs (dependencies ctxt false NONE description lhs rhs) end;
 
 fun add_deps_global a x y thy = add_deps (Syntax.init_pretty_global thy) a x y thy;
 
 fun specify_const decl thy =
   let val (t as Const const, thy') = Sign.declare_const_global decl thy;
-  in (t, add_deps_global "" const [] thy') end;
+  in (t, add_deps_global "" (DConst const) [] thy') end;
 
 
 (* overloading *)
@@ -271,15 +283,20 @@
 
 local
 
+fun fold_type_constr f (Type (name, Ts)) = f (name,Ts) #> fold (fold_type_constr f) Ts
+  | fold_type_constr _ _ = I;
+
 fun check_def ctxt thy unchecked overloaded (b, tm) defs =
   let
     val name = Sign.full_name thy b;
     val ((lhs, rhs), _) = Primitive_Defs.dest_def ctxt Term.is_Const (K false) (K false) tm
       handle TERM (msg, _) => error msg;
     val lhs_const = Term.dest_Const (Term.head_of lhs);
-    val rhs_consts = fold_aterms (fn Const const => insert (op =) const | _ => I) rhs [];
+    val rhs_consts = fold_aterms (fn Const const => insert (op =) (DConst const) | _ => I) rhs [];
+    val rhs_types = fold_types (fold_type_constr (insert (op =) o DType)) rhs []
+    val rhs_deps = rhs_consts @ rhs_types
     val _ = check_overloading ctxt overloaded lhs_const;
-  in defs |> dependencies ctxt unchecked (SOME name) name lhs_const rhs_consts end
+  in defs |> dependencies ctxt unchecked (SOME name) name (DConst lhs_const) rhs_deps end
   handle ERROR msg => cat_error msg (Pretty.string_of (Pretty.block
    [Pretty.str ("The error(s) above occurred in definition " ^ Binding.print b ^ ":"),
     Pretty.fbrk, Pretty.quote (Syntax.pretty_term ctxt tm)]));