src/HOL/Tools/inductive_codegen.ML

              eqns = eqns |> Symtab.map_default (s, [])
                (AList.update Thm.eq_thm_prop (thm, thyname_of s))} thy
       | _ => (warn thm; thy))
     | SOME (Const (s, _), _) =>
         let
-          val cs = foldr OldTerm.add_term_consts [] (prems_of thm);
+          val cs = fold Term.add_const_names (Thm.prems_of thm) [];
           val rules = Symtab.lookup_list intros s;
           val nparms = (case optnparms of
             SOME k => k
           | NONE => (case rules of
              [] => (case try (InductivePackage.the_inductive (ProofContext.init thy)) s of

     else (case get_clauses thy name of
         NONE => gr
       | SOME (names, thyname, nparms, intrs) =>
           mk_ind_def thy defs gr dep names (if_library thyname module)
             [] (prep_intrs intrs) nparms))
-            (gr, foldr OldTerm.add_term_consts [] ts)
+            (gr, fold Term.add_const_names ts [])
 
 and mk_ind_def thy defs gr dep names module modecs intrs nparms =
   add_edge_acyclic (hd names, dep) gr handle
     Graph.CYCLES (xs :: _) =>
       error ("InductiveCodegen: illegal cyclic dependencies:\n" ^ commas xs)