src/HOL/Tools/inductive_package.ML
changeset 29581 b3b33e0298eb
parent 29388 79eb3649ca9e
child 29863 dadad1831e9d
--- a/src/HOL/Tools/inductive_package.ML	Wed Jan 21 16:47:31 2009 +0100
+++ b/src/HOL/Tools/inductive_package.ML	Wed Jan 21 16:47:32 2009 +0100
@@ -38,17 +38,17 @@
     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
@@ -63,16 +63,16 @@
 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 ->
@@ -720,13 +720,13 @@
   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}