src/ZF/Tools/datatype_package.ML

--- a/src/ZF/Tools/datatype_package.ML	Mon Feb 11 15:19:17 2008 +0100
+++ b/src/ZF/Tools/datatype_package.ML	Mon Feb 11 15:40:21 2008 +0100
@@ -49,7 +49,7 @@
 fun add_datatype_i (dom_sum, rec_tms) con_ty_lists (monos, type_intrs, type_elims) thy =
  let
   val dummy = (*has essential ancestors?*)
-    Theory.requires thy "Datatype" "(co)datatype definitions";
+    Theory.requires thy "Datatype_ZF" "(co)datatype definitions";
 
   val rec_hds = map head_of rec_tms;