src/HOL/Tools/inductive_package.ML
changeset 15703 727ef1b8b3ee
parent 15574 b1d1b5bfc464
child 15705 b5edb9dcec9a
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Wed Apr 13 09:48:41 2005 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Wed Apr 13 18:34:22 2005 +0200
     1.3 @@ -44,14 +44,14 @@
     1.4    val inductive_forall_name: string
     1.5    val inductive_forall_def: thm
     1.6    val rulify: thm -> thm
     1.7 -  val inductive_cases: ((bstring * Args.src list) * string list) list -> theory -> theory
     1.8 +  val inductive_cases: ((bstring * Attrib.src list) * string list) list -> theory -> theory
     1.9    val inductive_cases_i: ((bstring * theory attribute list) * term list) list -> theory -> theory
    1.10    val add_inductive_i: bool -> bool -> bstring -> bool -> bool -> bool -> term list ->
    1.11      ((bstring * term) * theory attribute list) list -> thm list -> theory -> theory *
    1.12        {defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
    1.13         intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
    1.14    val add_inductive: bool -> bool -> string list ->
    1.15 -    ((bstring * string) * Args.src list) list -> (thmref * Args.src list) list ->
    1.16 +    ((bstring * string) * Attrib.src list) list -> (thmref * Attrib.src list) list ->
    1.17      theory -> theory *
    1.18        {defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
    1.19         intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}