1.1 --- a/src/ZF/Tools/inductive_package.ML	Wed Dec 03 21:00:39 2008 -0800
     1.2 +++ b/src/ZF/Tools/inductive_package.ML	Thu Dec 04 14:43:33 2008 +0100
     1.3 @@ -29,10 +29,10 @@
     1.4    (*Insert definitions for the recursive sets, which
     1.5       must *already* be declared as constants in parent theory!*)
     1.6    val add_inductive_i: bool -> term list * term ->
     1.7 -    ((Name.binding * term) * attribute list) list ->
     1.8 +    ((Binding.T * term) * attribute list) list ->
     1.9      thm list * thm list * thm list * thm list -> theory -> theory * inductive_result
    1.10    val add_inductive: string list * string ->
    1.11 -    ((Name.binding * string) * Attrib.src list) list ->
    1.12 +    ((Binding.T * string) * Attrib.src list) list ->
    1.13      (Facts.ref * Attrib.src list) list * (Facts.ref * Attrib.src list) list *
    1.14      (Facts.ref * Attrib.src list) list * (Facts.ref * Attrib.src list) list ->
    1.15      theory -> theory * inductive_result