1.1 --- a/src/HOL/SPARK/Tools/spark_vcs.ML	Fri Dec 16 22:07:03 2011 +0100
     1.2 +++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Sat Dec 17 12:10:37 2011 +0100
     1.3 @@ -159,8 +159,8 @@
     1.4  
     1.5  fun add_enum_type tyname tyname' thy =
     1.6    let
     1.7 -    val {case_name, ...} = the (Datatype_Data.get_info thy tyname');
     1.8 -    val cs = map Const (the (Datatype_Data.get_constrs thy tyname'));
     1.9 +    val {case_name, ...} = the (Datatype.get_info thy tyname');
    1.10 +    val cs = map Const (the (Datatype.get_constrs thy tyname'));
    1.11      val k = length cs;
    1.12      val T = Type (tyname', []);
    1.13      val p = Const (@{const_name pos}, T --> HOLogic.intT);
    1.14 @@ -195,7 +195,7 @@
    1.15        (fn _ =>
    1.16           rtac @{thm subset_antisym} 1 THEN
    1.17           rtac @{thm subsetI} 1 THEN
    1.18 -         Datatype_Aux.exh_tac (K (#exhaust (Datatype_Data.the_info
    1.19 +         Datatype_Aux.exh_tac (K (#exhaust (Datatype.the_info
    1.20             (Proof_Context.theory_of lthy) tyname'))) 1 THEN
    1.21           ALLGOALS (asm_full_simp_tac (simpset_of lthy)));
    1.22  
    1.23 @@ -311,7 +311,7 @@
    1.24                   tyname)
    1.25                end
    1.26            | SOME (T as Type (tyname, [])) =>
    1.27 -              (case Datatype_Data.get_constrs thy tyname of
    1.28 +              (case Datatype.get_constrs thy tyname of
    1.29                   NONE => assoc_ty_err thy T s "is not a datatype"
    1.30                 | SOME cs =>
    1.31                     let
    1.32 @@ -325,7 +325,7 @@
    1.33                         NONE => (thy, tyname)
    1.34                       | SOME msg => assoc_ty_err thy T s msg
    1.35                     end));
    1.36 -        val cs = map Const (the (Datatype_Data.get_constrs thy' tyname))
    1.37 +        val cs = map Const (the (Datatype.get_constrs thy' tyname));
    1.38        in
    1.39          ((fold (Symtab.update_new o apsnd (rpair s)) (els ~~ cs) tab,
    1.40            fold Name.declare els ctxt),
    1.41 @@ -825,7 +825,7 @@
    1.42                handle Symtab.DUP _ => error ("SPARK type " ^ s ^
    1.43                  " already associated with type")) |>
    1.44        (fn thy' =>
    1.45 -         case Datatype_Data.get_constrs thy' tyname of
    1.46 +         case Datatype.get_constrs thy' tyname of
    1.47             NONE => thy'
    1.48           | SOME cs =>
    1.49               if null Ts then