src/HOL/Tools/TFL/thry.ML

 (*---------------------------------------------------------------------------
  * Get information about datatypes
  *---------------------------------------------------------------------------*)
 
 fun match_info thy dtco =
-  case (Datatype.get_datatype thy dtco,
-         Datatype.get_datatype_constrs thy dtco) of
+  case (Datatype.get_info thy dtco,
+         Datatype.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_datatype thy dtco of
+fun induct_info thy dtco = case Datatype.get_info thy dtco of
         NONE => NONE
       | SOME {nchotomy, ...} =>
           SOME {nchotomy = nchotomy,
-                constructors = (map Const o the o Datatype.get_datatype_constrs thy) dtco};
+                constructors = (map Const o the o Datatype.get_constrs thy) dtco};
 
 fun extract_info thy =
- let val infos = (map snd o Symtab.dest o Datatype.get_datatypes) thy
+ let val infos = (map snd o Symtab.dest o Datatype.get_all) 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;