--- a/src/ZF/Tools/inductive_package.ML Mon Jan 24 18:11:06 2005 +0100
+++ b/src/ZF/Tools/inductive_package.ML Mon Jan 24 18:12:22 2005 +0100
@@ -35,8 +35,8 @@
-> thm list * thm list * thm list * thm list -> theory -> theory * inductive_result
val add_inductive: string list * string ->
((bstring * string) * Args.src list) list ->
- (xstring * Args.src list) list * (xstring * Args.src list) list *
- (xstring * Args.src list) list * (xstring * Args.src list) list ->
+ (thmref * Args.src list) list * (thmref * Args.src list) list *
+ (thmref * Args.src list) list * (thmref * Args.src list) list ->
theory -> theory * inductive_result
end;