clarified internal theory dependencies;
authorwenzelm
Thu Feb 21 20:10:34 2002 +0100 (2002-02-21)
changeset 12922ed70a600f0ea
parent 12921 b7b0daf0d882
child 12923 9ba7c5358fa0
clarified internal theory dependencies;
src/HOL/Tools/datatype_package.ML
src/HOL/Tools/datatype_rep_proofs.ML
src/HOL/Tools/inductive_package.ML
     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  
     2.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Thu Feb 21 20:10:05 2002 +0100
     2.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Thu Feb 21 20:10:34 2002 +0100
     2.3 @@ -44,7 +44,9 @@
     2.4  fun representation_proofs flat_names (dt_info : datatype_info Symtab.table)
     2.5        new_type_names descr sorts types_syntax constr_syntax case_names_induct thy =
     2.6    let
     2.7 -    val Datatype_thy = theory "Datatype";
     2.8 +    val Datatype_thy =
     2.9 +      if PureThy.get_name thy = "Datatype" then thy
    2.10 +      else theory "Datatype";
    2.11      val node_name = "Datatype_Universe.node";
    2.12      val In0_name = "Datatype_Universe.In0";
    2.13      val In1_name = "Datatype_Universe.In1";
     3.1 --- a/src/HOL/Tools/inductive_package.ML	Thu Feb 21 20:10:05 2002 +0100
     3.2 +++ b/src/HOL/Tools/inductive_package.ML	Thu Feb 21 20:10:34 2002 +0100
     3.3 @@ -614,9 +614,12 @@
     3.4  
     3.5      val sign = Theory.sign_of thy;
     3.6  
     3.7 -    val sum_case_rewrites = (case ThyInfo.lookup_theory "Datatype" of
     3.8 -        None => []
     3.9 -      | Some thy' => map mk_meta_eq (PureThy.get_thms thy' "sum.cases"));
    3.10 +    val sum_case_rewrites =
    3.11 +      (if PureThy.get_name thy = "Datatype" then PureThy.get_thms thy "sum.cases"
    3.12 +        else
    3.13 +          (case ThyInfo.lookup_theory "Datatype" of
    3.14 +            None => []
    3.15 +          | Some thy' => PureThy.get_thms thy' "sum.cases")) |> map mk_meta_eq;
    3.16  
    3.17      val (preds, ind_prems, mutual_ind_concl, factors) =
    3.18        mk_indrule cs cTs params intr_ts;