src/HOL/Tools/datatype_package.ML
changeset 20820 58693343905f
parent 20715 c1f16b427d86
child 21045 66d6d1b0ddfa
--- a/src/HOL/Tools/datatype_package.ML	Sun Oct 01 22:19:21 2006 +0200
+++ b/src/HOL/Tools/datatype_package.ML	Sun Oct 01 22:19:23 2006 +0200
@@ -927,7 +927,7 @@
 
 fun gen_add_datatype prep_typ err flat_names new_type_names dts thy =
   let
-    val _ = Theory.requires thy "Datatype_Universe" "datatype definitions";
+    val _ = Theory.requires thy "Datatype" "datatype definitions";
 
     (* this theory is used just for parsing *)