--- a/src/HOL/Tools/TFL/thry.ML Thu Jun 18 18:31:14 2009 -0700
+++ b/src/HOL/Tools/TFL/thry.ML Fri Jun 19 17:23:21 2009 +0200
@@ -60,20 +60,20 @@
*---------------------------------------------------------------------------*)
fun match_info thy dtco =
- case (DatatypePackage.get_datatype thy dtco,
- DatatypePackage.get_datatype_constrs thy dtco) of
+ case (Datatype.get_datatype thy dtco,
+ Datatype.get_datatype_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 DatatypePackage.get_datatype thy dtco of
+fun induct_info thy dtco = case Datatype.get_datatype thy dtco of
NONE => NONE
| SOME {nchotomy, ...} =>
SOME {nchotomy = nchotomy,
- constructors = (map Const o the o DatatypePackage.get_datatype_constrs thy) dtco};
+ constructors = (map Const o the o Datatype.get_datatype_constrs thy) dtco};
fun extract_info thy =
- let val infos = (map snd o Symtab.dest o DatatypePackage.get_datatypes) thy
+ let val infos = (map snd o Symtab.dest o Datatype.get_datatypes) thy
in {case_congs = map (mk_meta_eq o #case_cong) infos,
case_rewrites = List.concat (map (map mk_meta_eq o #case_rewrites) infos)}
end;