--- a/src/HOL/Tools/TFL/thry.ML Mon Sep 01 16:17:46 2014 +0200
+++ b/src/HOL/Tools/TFL/thry.ML Mon Sep 01 16:17:46 2014 +0200
@@ -58,20 +58,20 @@
*---------------------------------------------------------------------------*)
fun match_info thy dtco =
- case (Datatype.get_info thy dtco,
- Datatype.get_constrs thy dtco) of
+ case (Datatype_Data.get_info thy dtco,
+ Datatype_Data.get_constrs thy dtco) of
(SOME { case_name, ... }, SOME constructors) =>
SOME {case_const = Const (case_name, Sign.the_const_type thy case_name), constructors = map Const constructors}
| _ => NONE;
-fun induct_info thy dtco = case Datatype.get_info thy dtco of
+fun induct_info thy dtco = case Datatype_Data.get_info thy dtco of
NONE => NONE
| SOME {nchotomy, ...} =>
SOME {nchotomy = nchotomy,
- constructors = (map Const o the o Datatype.get_constrs thy) dtco};
+ constructors = (map Const o the o Datatype_Data.get_constrs thy) dtco};
fun extract_info thy =
- let val infos = map snd (Symtab.dest (Datatype.get_all thy))
+ let val infos = map snd (Symtab.dest (Datatype_Data.get_all thy))
in {case_congs = map (mk_meta_eq o #case_cong) infos,
case_rewrites = maps (map mk_meta_eq o #case_rewrites) infos}
end;