--- a/src/HOL/SPARK/Tools/spark_vcs.ML Mon Sep 01 16:17:46 2014 +0200
+++ b/src/HOL/SPARK/Tools/spark_vcs.ML Mon Sep 01 16:17:46 2014 +0200
@@ -173,8 +173,8 @@
fun add_enum_type tyname tyname' thy =
let
- val {case_name, ...} = the (Datatype.get_info thy tyname');
- val cs = map Const (the (Datatype.get_constrs thy tyname'));
+ val {case_name, ...} = the (Datatype_Data.get_info thy tyname');
+ val cs = map Const (the (Datatype_Data.get_constrs thy tyname'));
val k = length cs;
val T = Type (tyname', []);
val p = Const (@{const_name pos}, T --> HOLogic.intT);
@@ -209,7 +209,7 @@
(fn _ =>
rtac @{thm subset_antisym} 1 THEN
rtac @{thm subsetI} 1 THEN
- Datatype_Aux.exh_tac (K (#exhaust (Datatype.the_info
+ Datatype_Aux.exh_tac (K (#exhaust (Datatype_Data.the_info
(Proof_Context.theory_of lthy) tyname'))) 1 THEN
ALLGOALS (asm_full_simp_tac lthy));
@@ -327,7 +327,7 @@
tyname)
end
| SOME (T as Type (tyname, []), cmap) =>
- (case Datatype.get_constrs thy tyname of
+ (case Datatype_Data.get_constrs thy tyname of
NONE => assoc_ty_err thy T s "is not a datatype"
| SOME cs =>
let val (prfx', _) = strip_prfx s
@@ -338,7 +338,7 @@
| SOME msg => assoc_ty_err thy T s msg
end)
| SOME (T, _) => assoc_ty_err thy T s "is not a datatype");
- val cs = map Const (the (Datatype.get_constrs thy' tyname));
+ val cs = map Const (the (Datatype_Data.get_constrs thy' tyname));
in
((fold (Symtab.update_new o apsnd (rpair s)) (els ~~ cs) tab,
fold Name.declare els ctxt),
@@ -888,7 +888,7 @@
handle Symtab.DUP _ => error ("SPARK type " ^ s ^
" already associated with type")) |>
(fn thy' =>
- case Datatype.get_constrs thy' tyname of
+ case Datatype_Data.get_constrs thy' tyname of
NONE => (case get_record_info thy' T of
NONE => thy'
| SOME {fields, ...} =>