src/HOL/Nominal/nominal_inductive.ML

       in
         (Logic.list_all (params', prem), (rev vs, subst_bounds (vs, prem)))
       end) prems);
 
     val ind_vars =
-      (Datatype_Prop.indexify_names (replicate (length atomTs) "pi") ~~
+      (Old_Datatype_Prop.indexify_names (replicate (length atomTs) "pi") ~~
        map NominalAtoms.mk_permT atomTs) @ [("z", fsT)];
     val ind_Ts = rev (map snd ind_vars);
 
     val concl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
       (map (fn (prem, (p, ts)) => HOLogic.mk_imp (prem,

         | SOME (th, _) => Seq.single th
       end;
     val thss = map (fn atom =>
       let val pi' = Free (pi, NominalAtoms.mk_permT (Type (atom, [])))
       in map (fn th => zero_var_indexes (th RS mp))
-        (Datatype_Aux.split_conj_thm (Goal.prove ctxt' [] []
+        (Old_Datatype_Aux.split_conj_thm (Goal.prove ctxt' [] []
           (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map (fn p =>
             let
               val (h, ts) = strip_comb p;
               val (ts1, ts2) = chop k ts
             in