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