src/HOL/Tools/Function/fundef_datatype.ML

       fun check_constr_pattern (Bound _) = ()
         | check_constr_pattern t =
           let
             val (hd, args) = strip_comb t
           in
-            (((case Datatype.datatype_of_constr thy (fst (dest_Const hd)) of
+            (((case Datatype.info_of_constr thy (fst (dest_Const hd)) of
                  SOME _ => ()
                | NONE => err "Non-constructor pattern")
               handle TERM ("dest_Const", _) => err "Non-constructor patterns");
              map check_constr_pattern args; 
              ())

              else filter_pats thy cons pvars pts
 
 
 fun inst_constrs_of thy (T as Type (name, _)) =
         map (fn (Cn,CT) => Envir.subst_TVars (Sign.typ_match thy (body_type CT, T) Vartab.empty) (Const (Cn, CT)))
-            (the (Datatype.get_datatype_constrs thy name))
+            (the (Datatype.get_constrs thy name))
   | inst_constrs_of thy _ = raise Match
 
 
 fun transform_pat thy avars c_assum ([] , thm) = raise Match
   | transform_pat thy avars c_assum (pat :: pats, thm) =

                                (pats, refl RS (inst_free (cterm_of thy pv) (cterm_of thy v) thm))) pts)
     else (* Cons case *)
          let
              val T = fastype_of v
              val (tname, _) = dest_Type T
-             val {exhaustion=case_thm, ...} = Datatype.the_datatype thy tname
+             val {exhaustion=case_thm, ...} = Datatype.the_info thy tname
              val constrs = inst_constrs_of thy T
              val c_cases = map (constr_case thy P idx (v :: vs) pts) constrs
          in
              inst_case_thm thy v P case_thm
                            |> fold (curry op COMP) c_cases