src/HOL/Tools/BNF/bnf_gfp.ML

           end;
 
         val Suc = Term.absdummy HOLogic.natT (Term.absfree hrec'
           (HOLogic.mk_tuple (map4 mk_Suc ss setssAs zs zs')));
 
-        val rhs = mk_nat_rec Zero Suc;
+        val rhs = mk_rec_nat Zero Suc;
       in
         fold_rev (Term.absfree o Term.dest_Free) ss rhs
       end;
 
     val ((hset_rec_frees, (_, hset_rec_def_frees)), (lthy, lthy_old)) =

         val hset_recT = Library.foldr (op -->) (Ts, HOLogic.natT --> hrecT);
       in
         mk_nthN n (Term.list_comb (Const (nth hset_recs (j - 1), hset_recT), args)) i
       end;
 
-    val hset_rec_0ss = mk_rec_simps n @{thm nat_rec_0_imp} hset_rec_defs;
-    val hset_rec_Sucss = mk_rec_simps n @{thm nat_rec_Suc_imp} hset_rec_defs;
+    val hset_rec_0ss = mk_rec_simps n @{thm rec_nat_0_imp} hset_rec_defs;
+    val hset_rec_Sucss = mk_rec_simps n @{thm rec_nat_Suc_imp} hset_rec_defs;
     val hset_rec_0ss' = transpose hset_rec_0ss;
     val hset_rec_Sucss' = transpose hset_rec_Sucss;
 
     fun hset_binds j = mk_internal_bs (hsetN ^ (if m = 1 then "" else string_of_int j))
     fun hset_bind i j = nth (hset_binds j) (i - 1);

           end;
 
         val Suc = Term.absdummy HOLogic.natT (Term.absfree Lev_rec'
           (HOLogic.mk_tuple (map5 mk_Suc ks ss setssAs zs zs')));
 
-        val rhs = mk_nat_rec Zero Suc;
+        val rhs = mk_rec_nat Zero Suc;
       in
         fold_rev (Term.absfree o Term.dest_Free) ss rhs
       end;
 
     val ((Lev_free, (_, Lev_def_free)), (lthy, lthy_old)) =