src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML

     let
       val s = Name.uu;
       val eq = Abs (Name.uu, T, HOLogic.mk_eq (Free (s, T), Bound 0));
     in
       Thm.instantiate' [] [SOME (Thm.cterm_of ctxt eq)] split
-      |> Drule.generalize (Symtab.empty, Symtab.make_set [s])
+      |> Drule.generalize (Names.empty, Names.make_set [s])
     end
   | _ => split);
 
 fun raw_code_single_tac ctxt distincts discIs splits split_asms m fun_ctr =
   let