--- a/src/ZF/Tools/datatype_package.ML Wed Mar 19 18:15:25 2008 +0100
+++ b/src/ZF/Tools/datatype_package.ML Wed Mar 19 22:27:57 2008 +0100
@@ -33,8 +33,8 @@
val add_datatype_i: term * term list -> Ind_Syntax.constructor_spec list list ->
thm list * thm list * thm list -> theory -> theory * inductive_result * datatype_result
val add_datatype: string * string list -> (string * string list * mixfix) list list ->
- (thmref * Attrib.src list) list * (thmref * Attrib.src list) list *
- (thmref * Attrib.src list) list -> theory -> theory * inductive_result * datatype_result
+ (Facts.ref * Attrib.src list) list * (Facts.ref * Attrib.src list) list *
+ (Facts.ref * Attrib.src list) list -> theory -> theory * inductive_result * datatype_result
end;
functor Add_datatype_def_Fun