src/ZF/Tools/datatype_package.ML

   (*Insert definitions for the recursive sets, which
      must *already* be declared as constants in parent theory!*)
   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 ->
-    (Facts.ref * Attrib.src list) list * (Facts.ref * Attrib.src list) list *
-    (Facts.ref * Attrib.src list) list -> theory -> theory * inductive_result * datatype_result
+    (Facts.ref * Token.src list) list * (Facts.ref * Token.src list) list *
+    (Facts.ref * Token.src list) list -> theory -> theory * inductive_result * datatype_result
 end;
 
 functor Add_datatype_def_Fun
  (structure Fp: FP and Pr : PR and CP: CARTPROD and Su : SU
   and Ind_Package : INDUCTIVE_PACKAGE