--- a/src/ZF/Tools/inductive_package.ML Wed Mar 19 18:15:25 2008 +0100
+++ b/src/ZF/Tools/inductive_package.ML Wed Mar 19 22:27:57 2008 +0100
@@ -33,8 +33,8 @@
thm list * thm list * thm list * thm list -> theory -> theory * inductive_result
val add_inductive: string list * string ->
((bstring * string) * Attrib.src list) list ->
- (thmref * Attrib.src list) list * (thmref * Attrib.src list) list *
- (thmref * Attrib.src list) list * (thmref * Attrib.src list) list ->
+ (Facts.ref * Attrib.src list) list * (Facts.ref * Attrib.src list) list *
+ (Facts.ref * Attrib.src list) list * (Facts.ref * Attrib.src list) list ->
theory -> theory * inductive_result
end;