src/HOL/Nominal/nominal_primrec.ML

           NONE => (warning ("No equation for constructor " ^ quote cname ^
             "\nin definition of function " ^ quote fname);
               (fnames', fnss', (Const (@{const_name undefined}, dummyT))::fns))
         | SOME (ls, cargs', rs, rhs, eq) =>
             let
-              val recs = filter (Datatype_Aux.is_rec_type o snd) (cargs' ~~ cargs);
+              val recs = filter (Old_Datatype_Aux.is_rec_type o snd) (cargs' ~~ cargs);
               val rargs = map fst recs;
               val subs = map (rpair dummyT o fst)
                 (rev (Term.rename_wrt_term rhs rargs));
               val (rhs', (fnames'', fnss'')) = subst (map2 (fn (x, y) => fn z =>
-                (Free x, (Datatype_Aux.body_index y, Free z))) recs subs) rhs (fnames', fnss')
+                (Free x, (Old_Datatype_Aux.body_index y, Free z))) recs subs) rhs (fnames', fnss')
                   handle RecError s => primrec_eq_err lthy s eq
             in (fnames'', fnss'', fold_rev absfree (cargs' @ subs) rhs' :: fns)
             end)
 
   in (case AList.lookup (op =) fnames i of

 fun get_fns fns ((i : int, (tname, _, constrs)), rec_name) (fs, defs) =
   case AList.lookup (op =) fns i of
      NONE =>
        let
          val dummy_fns = map (fn (_, cargs) => Const (@{const_name undefined},
-           replicate (length cargs + length (filter Datatype_Aux.is_rec_type cargs))
+           replicate (length cargs + length (filter Old_Datatype_Aux.is_rec_type cargs))
              dummyT ---> HOLogic.unitT)) constrs;
          val _ = warning ("No function definition for datatype " ^ quote tname)
        in
          (dummy_fns @ fs, defs)
        end