diff -r 02cc5fa9c5f1 -r 0aaeb5520f2f src/HOL/SPARK/Tools/spark_vcs.ML
--- a/src/HOL/SPARK/Tools/spark_vcs.ML	Fri Dec 16 22:07:03 2011 +0100
+++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Sat Dec 17 12:10:37 2011 +0100
@@ -159,8 +159,8 @@
 
 fun add_enum_type tyname tyname' thy =
   let
-    val {case_name, ...} = the (Datatype_Data.get_info thy tyname');
-    val cs = map Const (the (Datatype_Data.get_constrs thy tyname'));
+    val {case_name, ...} = the (Datatype.get_info thy tyname');
+    val cs = map Const (the (Datatype.get_constrs thy tyname'));
     val k = length cs;
     val T = Type (tyname', []);
     val p = Const (@{const_name pos}, T --> HOLogic.intT);
@@ -195,7 +195,7 @@
       (fn _ =>
          rtac @{thm subset_antisym} 1 THEN
          rtac @{thm subsetI} 1 THEN
-         Datatype_Aux.exh_tac (K (#exhaust (Datatype_Data.the_info
+         Datatype_Aux.exh_tac (K (#exhaust (Datatype.the_info
            (Proof_Context.theory_of lthy) tyname'))) 1 THEN
          ALLGOALS (asm_full_simp_tac (simpset_of lthy)));
 
@@ -311,7 +311,7 @@
                  tyname)
               end
           | SOME (T as Type (tyname, [])) =>
-              (case Datatype_Data.get_constrs thy tyname of
+              (case Datatype.get_constrs thy tyname of
                  NONE => assoc_ty_err thy T s "is not a datatype"
                | SOME cs =>
                    let
@@ -325,7 +325,7 @@
                        NONE => (thy, tyname)
                      | SOME msg => assoc_ty_err thy T s msg
                    end));
-        val cs = map Const (the (Datatype_Data.get_constrs thy' tyname))
+        val cs = map Const (the (Datatype.get_constrs thy' tyname));
       in
         ((fold (Symtab.update_new o apsnd (rpair s)) (els ~~ cs) tab,
           fold Name.declare els ctxt),
@@ -825,7 +825,7 @@
               handle Symtab.DUP _ => error ("SPARK type " ^ s ^
                 " already associated with type")) |>
       (fn thy' =>
-         case Datatype_Data.get_constrs thy' tyname of
+         case Datatype.get_constrs thy' tyname of
            NONE => thy'
          | SOME cs =>
              if null Ts then