src/HOL/Nominal/nominal_datatype.ML

 val Collect_False_empty = @{thm empty_def [THEN sym, THEN eq_reflection]};
 val empty_iff = @{thm empty_iff};
 
 open NominalAtoms;
 
-(** FIXME: Datatype should export this function **)
-
-local
-
-fun dt_recs (Datatype_Aux.DtTFree _) = []
-  | dt_recs (Datatype_Aux.DtType (_, dts)) = maps dt_recs dts
-  | dt_recs (Datatype_Aux.DtRec i) = [i];
-
-fun dt_cases (descr: Datatype_Aux.descr) (_, args, constrs) =
-  let
-    fun the_bname i = Long_Name.base_name (#1 (the (AList.lookup (op =) descr i)));
-    val bnames = map the_bname (distinct op = (maps dt_recs args));
-  in map (fn (c, _) => space_implode "_" (Long_Name.base_name c :: bnames)) constrs end;
-
-
-fun induct_cases descr =
-  Datatype_Prop.indexify_names (maps (dt_cases descr) (map #2 descr));
-
-fun exhaust_cases descr i = dt_cases descr (the (AList.lookup (op =) descr i));
-
-in
-
-fun mk_case_names_induct descr = Rule_Cases.case_names (induct_cases descr);
-
-fun mk_case_names_exhausts descr new =
-  map (Rule_Cases.case_names o exhaust_cases descr o #1)
-    (filter (fn ((_, (name, _, _))) => member (op =) new name) descr);
-
-end;
 
 (* theory data *)
 
 type descr =
   (int * (string * Datatype_Aux.dtyp list *

            [REPEAT (eresolve_tac Abs_inverse_thms' 1),
             simp_tac (HOL_basic_ss addsimps [Thm.symmetric r]) 1,
             DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE etac allE 1)]))
                 (prems ~~ constr_defs))]);
 
-    val case_names_induct = mk_case_names_induct descr'';
+    val case_names_induct = Datatype_Data.mk_case_names_induct descr'';
 
     (**** prove that new datatypes have finite support ****)
 
     val _ = warning "proving finite support for the new datatype";