src/HOL/Tools/inductive_package.ML

     thm list list * local_theory
   val inductive_cases_i: (Attrib.binding * term list) list -> local_theory ->
     thm list list * local_theory
   type inductive_flags
   val add_inductive_i:
-    inductive_flags -> ((Binding.T * typ) * mixfix) list ->
+    inductive_flags -> ((binding * typ) * mixfix) list ->
     (string * typ) list -> (Attrib.binding * term) list -> thm list -> local_theory ->
     inductive_result * local_theory
   val add_inductive: bool -> bool ->
-    (Binding.T * string option * mixfix) list ->
-    (Binding.T * string option * mixfix) list ->
+    (binding * string option * mixfix) list ->
+    (binding * string option * mixfix) list ->
     (Attrib.binding * string) list ->
     (Facts.ref * Attrib.src list) list ->
     bool -> local_theory -> inductive_result * local_theory
   val add_inductive_global: string -> inductive_flags ->
-    ((Binding.T * typ) * mixfix) list -> (string * typ) list -> (Attrib.binding * term) list ->
+    ((binding * typ) * mixfix) list -> (string * typ) list -> (Attrib.binding * term) list ->
     thm list -> theory -> inductive_result * theory
   val arities_of: thm -> (string * int) list
   val params_of: thm -> term list
   val partition_rules: thm -> thm list -> (string * thm list) list
   val partition_rules': thm -> (thm * 'a) list -> (string * (thm * 'a) list) list

 
 signature INDUCTIVE_PACKAGE =
 sig
   include BASIC_INDUCTIVE_PACKAGE
   type add_ind_def
-  val declare_rules: string -> Binding.T -> bool -> bool -> string list ->
-    thm list -> Binding.T list -> Attrib.src list list -> (thm * string list) list ->
+  val declare_rules: string -> binding -> bool -> bool -> string list ->
+    thm list -> binding list -> Attrib.src list list -> (thm * string list) list ->
     thm -> local_theory -> thm list * thm list * thm * local_theory
   val add_ind_def: add_ind_def
   val gen_add_inductive_i: add_ind_def -> inductive_flags ->
-    ((Binding.T * typ) * mixfix) list -> (string * typ) list -> (Attrib.binding * term) list ->
+    ((binding * typ) * mixfix) list -> (string * typ) list -> (Attrib.binding * term) list ->
     thm list -> local_theory -> inductive_result * local_theory
   val gen_add_inductive: add_ind_def -> bool -> bool ->
-    (Binding.T * string option * mixfix) list ->
-    (Binding.T * string option * mixfix) list ->
+    (binding * string option * mixfix) list ->
+    (binding * string option * mixfix) list ->
     (Attrib.binding * string) list -> (Facts.ref * Attrib.src list) list ->
     bool -> local_theory -> inductive_result * local_theory
   val gen_ind_decl: add_ind_def -> bool ->
     OuterParse.token list -> (bool -> local_theory -> local_theory) * OuterParse.token list
 end;

              Attrib.internal (K (Induct.induct_pred name))])))] |> snd
       end
   in (intrs', elims', induct', ctxt3) end;
 
 type inductive_flags =
-  {quiet_mode: bool, verbose: bool, kind: string, alt_name: Binding.T,
+  {quiet_mode: bool, verbose: bool, kind: string, alt_name: binding,
    coind: bool, no_elim: bool, no_ind: bool, skip_mono: bool, fork_mono: bool}
 
 type add_ind_def =
   inductive_flags ->
   term list -> (Attrib.binding * term) list -> thm list ->
-  term list -> (Binding.T * mixfix) list ->
+  term list -> (binding * mixfix) list ->
   local_theory -> inductive_result * local_theory
 
 fun add_ind_def {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono}
     cs intros monos params cnames_syn ctxt =
   let