src/ZF/Tools/ind_cases.ML

--- a/src/ZF/Tools/ind_cases.ML	Tue Sep 02 14:10:45 2008 +0200
+++ b/src/ZF/Tools/ind_cases.ML	Tue Sep 02 16:55:33 2008 +0200
@@ -8,7 +8,7 @@
 signature IND_CASES =
 sig
   val declare: string -> (simpset -> cterm -> thm) -> theory -> theory
-  val inductive_cases: ((Name.binding * Attrib.src list) * string list) list -> theory -> theory
+  val inductive_cases: (Attrib.binding * string list) list -> theory -> theory
   val setup: theory -> theory
 end;