--- a/src/ZF/Tools/induct_tacs.ML Wed Apr 13 09:48:41 2005 +0200
+++ b/src/ZF/Tools/induct_tacs.ML Wed Apr 13 18:34:22 2005 +0200
@@ -13,8 +13,8 @@
val induct_tac: string -> int -> tactic
val exhaust_tac: string -> int -> tactic
val rep_datatype_i: thm -> thm -> thm list -> thm list -> theory -> theory
- val rep_datatype: thmref * Args.src list -> thmref * Args.src list ->
- (thmref * Args.src list) list -> (thmref * Args.src list) list -> theory -> theory
+ val rep_datatype: thmref * Attrib.src list -> thmref * Attrib.src list ->
+ (thmref * Attrib.src list) list -> (thmref * Attrib.src list) list -> theory -> theory
val setup: (theory -> theory) list
end;