clarified internal theory dependencies;

--- a/src/HOL/Tools/datatype_package.ML	Thu Feb 21 20:10:05 2002 +0100
+++ b/src/HOL/Tools/datatype_package.ML	Thu Feb 21 20:10:34 2002 +0100
@@ -665,6 +665,8 @@
 
 fun gen_rep_datatype apply_theorems alt_names raw_distinct raw_inject raw_induction thy0 =
   let
+    val _ = Theory.requires thy0 "Inductive" "datatype representations";
+
     fun app_thmss srcs thy = foldl_map (fn (thy, x) => apply_theorems x thy) (thy, srcs);
     fun app_thm src thy = apsnd Library.hd (apply_theorems [src] thy);
 
@@ -773,7 +775,7 @@
 
 fun gen_add_datatype prep_typ flat_names new_type_names dts thy =
   let
-    val _ = Theory.requires thy "Datatype" "datatype definitions";
+    val _ = Theory.requires thy "Datatype_Universe" "datatype definitions";
 
     (* this theory is used just for parsing *)
 

--- a/src/HOL/Tools/datatype_rep_proofs.ML	Thu Feb 21 20:10:05 2002 +0100
+++ b/src/HOL/Tools/datatype_rep_proofs.ML	Thu Feb 21 20:10:34 2002 +0100
@@ -44,7 +44,9 @@
 fun representation_proofs flat_names (dt_info : datatype_info Symtab.table)
       new_type_names descr sorts types_syntax constr_syntax case_names_induct thy =
   let
-    val Datatype_thy = theory "Datatype";
+    val Datatype_thy =
+      if PureThy.get_name thy = "Datatype" then thy
+      else theory "Datatype";
     val node_name = "Datatype_Universe.node";
     val In0_name = "Datatype_Universe.In0";
     val In1_name = "Datatype_Universe.In1";

--- a/src/HOL/Tools/inductive_package.ML	Thu Feb 21 20:10:05 2002 +0100
+++ b/src/HOL/Tools/inductive_package.ML	Thu Feb 21 20:10:34 2002 +0100
@@ -614,9 +614,12 @@
 
     val sign = Theory.sign_of thy;
 
-    val sum_case_rewrites = (case ThyInfo.lookup_theory "Datatype" of
-        None => []
-      | Some thy' => map mk_meta_eq (PureThy.get_thms thy' "sum.cases"));
+    val sum_case_rewrites =
+      (if PureThy.get_name thy = "Datatype" then PureThy.get_thms thy "sum.cases"
+        else
+          (case ThyInfo.lookup_theory "Datatype" of
+            None => []
+          | Some thy' => PureThy.get_thms thy' "sum.cases")) |> map mk_meta_eq;
 
     val (preds, ind_prems, mutual_ind_concl, factors) =
       mk_indrule cs cTs params intr_ts;