--- a/src/HOL/Nominal/nominal_datatype.ML Fri Dec 16 22:07:03 2011 +0100
+++ b/src/HOL/Nominal/nominal_datatype.ML Sat Dec 17 12:10:37 2011 +0100
@@ -1045,7 +1045,7 @@
DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE etac allE 1)]))
(prems ~~ constr_defs))]);
- val case_names_induct = Datatype_Data.mk_case_names_induct descr'';
+ val case_names_induct = Datatype.mk_case_names_induct descr'';
(**** prove that new datatypes have finite support ****)
--- 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
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Fri Dec 16 22:07:03 2011 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Sat Dec 17 12:10:37 2011 +0100
@@ -623,7 +623,7 @@
|> Local_Defs.unfold ctxt [@{thm atomize_conjL[symmetric]},
@{thm atomize_all[symmetric]}, @{thm atomize_imp[symmetric]}]
-fun find_split_thm thy (Const (name, T)) = Option.map #split (Datatype_Data.info_of_case thy name)
+fun find_split_thm thy (Const (name, T)) = Option.map #split (Datatype.info_of_case thy name)
| find_split_thm thy _ = NONE
(* lifting term operations to theorems *)
@@ -901,7 +901,7 @@
(*** this should be part of the datatype package ***)
fun datatype_names_of_case_name thy case_name =
- map (#1 o #2) (#descr (the (Datatype_Data.info_of_case thy case_name)))
+ map (#1 o #2) (#descr (the (Datatype.info_of_case thy case_name)))
fun make_case_distribs case_names descr thy =
let
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Fri Dec 16 22:07:03 2011 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Sat Dec 17 12:10:37 2011 +0100
@@ -847,7 +847,7 @@
case T of
TFree _ => NONE
| Type (Tcon, _) =>
- (case Datatype_Data.get_constrs (Proof_Context.theory_of ctxt) Tcon of
+ (case Datatype.get_constrs (Proof_Context.theory_of ctxt) Tcon of
NONE => NONE
| SOME cs =>
(case strip_comb t of
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML Fri Dec 16 22:07:03 2011 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML Sat Dec 17 12:10:37 2011 +0100
@@ -142,7 +142,7 @@
| restrict_pattern' thy ((T as TFree _, t) :: Tts) free_names =
replace_term_and_restrict thy T t Tts free_names
| restrict_pattern' thy ((T as Type (Tcon, Ts), t) :: Tts) free_names =
- case Datatype_Data.get_constrs thy Tcon of
+ case Datatype.get_constrs thy Tcon of
NONE => replace_term_and_restrict thy T t Tts free_names
| SOME constrs => (case strip_comb t of
(Const (s, _), ats) => (case AList.lookup (op =) constrs s of
--- a/src/HOL/Tools/list_to_set_comprehension.ML Fri Dec 16 22:07:03 2011 +0100
+++ b/src/HOL/Tools/list_to_set_comprehension.ML Sat Dec 17 12:10:37 2011 +0100
@@ -93,7 +93,7 @@
in
(case try dest_Const case_const of
SOME (c, T) =>
- (case Datatype_Data.info_of_case thy c of
+ (case Datatype.info_of_case thy c of
SOME _ =>
(case possible_index_of_singleton_case (fst (split_last args)) of
SOME i =>
@@ -178,7 +178,7 @@
val (vs, body) = strip_abs (Pattern.eta_long (map snd bound_vs) cont)
val x' = incr_boundvars (length vs) x
val eqs' = map (incr_boundvars (length vs)) eqs
- val (constr_name, _) = nth (the (Datatype_Data.get_constrs thy (fst (dest_Type T)))) i
+ val (constr_name, _) = nth (the (Datatype.get_constrs thy (fst (dest_Type T)))) i
val constr_t =
list_comb
(Const (constr_name, map snd vs ---> T), map Bound (((length vs) - 1) downto 0))