src/ZF/Tools/ind_cases.ML
changeset 15703 727ef1b8b3ee
parent 15531 08c8dad8e399
child 15705 b5edb9dcec9a
     1.1 --- a/src/ZF/Tools/ind_cases.ML	Wed Apr 13 09:48:41 2005 +0200
     1.2 +++ b/src/ZF/Tools/ind_cases.ML	Wed Apr 13 18:34:22 2005 +0200
     1.3 @@ -8,7 +8,7 @@
     1.4  signature IND_CASES =
     1.5  sig
     1.6    val declare: string -> (simpset -> cterm -> thm) -> theory -> theory
     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 setup: (theory -> theory) list
    1.10  end;
    1.11