src/HOL/Tools/datatype_package/datatype_codegen.ML

--- a/src/HOL/Tools/datatype_package/datatype_codegen.ML	Thu Jun 18 18:31:14 2009 -0700
+++ b/src/HOL/Tools/datatype_package/datatype_codegen.ML	Fri Jun 19 17:23:21 2009 +0200
@@ -276,12 +276,12 @@
 
 fun datatype_codegen thy defs dep module brack t gr = (case strip_comb t of
    (c as Const (s, T), ts) =>
-     (case DatatypePackage.datatype_of_case thy s of
+     (case Datatype.datatype_of_case thy s of
         SOME {index, descr, ...} =>
           if is_some (get_assoc_code thy (s, T)) then NONE else
           SOME (pretty_case thy defs dep module brack
             (#3 (the (AList.lookup op = descr index))) c ts gr )
-      | NONE => case (DatatypePackage.datatype_of_constr thy s, strip_type T) of
+      | NONE => case (Datatype.datatype_of_constr thy s, strip_type T) of
         (SOME {index, descr, ...}, (_, U as Type (tyname, _))) =>
           if is_some (get_assoc_code thy (s, T)) then NONE else
           let
@@ -296,7 +296,7 @@
  | _ => NONE);
 
 fun datatype_tycodegen thy defs dep module brack (Type (s, Ts)) gr =
-      (case DatatypePackage.get_datatype thy s of
+      (case Datatype.get_datatype thy s of
          NONE => NONE
        | SOME {descr, sorts, ...} =>
            if is_some (get_assoc_type thy s) then NONE else
@@ -331,7 +331,7 @@
 fun mk_case_cert thy tyco =
   let
     val raw_thms =
-      (#case_rewrites o DatatypePackage.the_datatype thy) tyco;
+      (#case_rewrites o Datatype.the_datatype thy) tyco;
     val thms as hd_thm :: _ = raw_thms
       |> Conjunction.intr_balanced
       |> Thm.unvarify
@@ -364,8 +364,8 @@
 
 fun mk_eq_eqns thy dtco =
   let
-    val (vs, cos) = DatatypePackage.the_datatype_spec thy dtco;
-    val { descr, index, inject = inject_thms, ... } = DatatypePackage.the_datatype thy dtco;
+    val (vs, cos) = Datatype.the_datatype_spec thy dtco;
+    val { descr, index, inject = inject_thms, ... } = Datatype.the_datatype thy dtco;
     val ty = Type (dtco, map TFree vs);
     fun mk_eq (t1, t2) = Const (@{const_name eq_class.eq}, ty --> ty --> HOLogic.boolT)
       $ t1 $ t2;
@@ -383,7 +383,7 @@
     val refl = HOLogic.mk_Trueprop (true_eq (Free ("x", ty), Free ("x", ty)));
     val simpset = Simplifier.context (ProofContext.init thy) (HOL_basic_ss
       addsimps (map Simpdata.mk_eq (@{thm eq} :: @{thm eq_True} :: inject_thms))
-      addsimprocs [DatatypePackage.distinct_simproc]);
+      addsimprocs [Datatype.distinct_simproc]);
     fun prove prop = SkipProof.prove_global thy [] [] prop (K (ALLGOALS (simp_tac simpset)))
       |> Simpdata.mk_eq;
   in map (rpair true o prove) (triv_injects @ injects @ distincts) @ [(prove refl, false)] end;
@@ -428,11 +428,11 @@
 
 fun add_all_code config dtcos thy =
   let
-    val (vs :: _, coss) = (split_list o map (DatatypePackage.the_datatype_spec thy)) dtcos;
+    val (vs :: _, coss) = (split_list o map (Datatype.the_datatype_spec thy)) dtcos;
     val any_css = map2 (mk_constr_consts thy vs) dtcos coss;
     val css = if exists is_none any_css then []
       else map_filter I any_css;
-    val case_rewrites = maps (#case_rewrites o DatatypePackage.the_datatype thy) dtcos;
+    val case_rewrites = maps (#case_rewrites o Datatype.the_datatype thy) dtcos;
     val certs = map (mk_case_cert thy) dtcos;
   in
     if null css then thy
@@ -450,6 +450,6 @@
 val setup = 
   add_codegen "datatype" datatype_codegen
   #> add_tycodegen "datatype" datatype_tycodegen
-  #> DatatypePackage.interpretation add_all_code
+  #> Datatype.interpretation add_all_code
 
 end;