src/HOL/Tools/datatype_package.ML
changeset 12922 ed70a600f0ea
parent 12876 a70df1e5bf10
child 13340 9b0332344ae2
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Thu Feb 21 20:10:05 2002 +0100
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Thu Feb 21 20:10:34 2002 +0100
     1.3 @@ -665,6 +665,8 @@
     1.4  
     1.5  fun gen_rep_datatype apply_theorems alt_names raw_distinct raw_inject raw_induction thy0 =
     1.6    let
     1.7 +    val _ = Theory.requires thy0 "Inductive" "datatype representations";
     1.8 +
     1.9      fun app_thmss srcs thy = foldl_map (fn (thy, x) => apply_theorems x thy) (thy, srcs);
    1.10      fun app_thm src thy = apsnd Library.hd (apply_theorems [src] thy);
    1.11  
    1.12 @@ -773,7 +775,7 @@
    1.13  
    1.14  fun gen_add_datatype prep_typ flat_names new_type_names dts thy =
    1.15    let
    1.16 -    val _ = Theory.requires thy "Datatype" "datatype definitions";
    1.17 +    val _ = Theory.requires thy "Datatype_Universe" "datatype definitions";
    1.18  
    1.19      (* this theory is used just for parsing *)
    1.20