src/HOL/Tools/TFL/thry.ML

 (*---------------------------------------------------------------------------
  * Get information about datatypes
  *---------------------------------------------------------------------------*)
 
 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;