diff -r 633fe7390c97 -r 612b7e0d6721 src/HOL/Library/code_lazy.ML
--- a/src/HOL/Library/code_lazy.ML	Thu Sep 09 10:40:57 2021 +0200
+++ b/src/HOL/Library/code_lazy.ML	Thu Sep 09 12:33:14 2021 +0200
@@ -122,7 +122,7 @@
         |> Conjunction.intr_balanced
         |> rewrite_rule ctxt [Thm.symmetric (Thm.assume assum)]
         |> Thm.implies_intr assum
-        |> Thm.generalize (Symtab.empty, Symtab.make_set params) 0
+        |> Thm.generalize (Names.empty, Names.make_set params) 0
         |> Axclass.unoverload ctxt
         |> Thm.varifyT_global
       end
@@ -495,7 +495,7 @@
       |> Drule.infer_instantiate' lthy10
          [SOME (Thm.cterm_of lthy10 (Const (\<^const_name>\<open>Pure.dummy_pattern\<close>, HOLogic.unitT --> lazy_type)))]
       |> Thm.generalize
-         (Symtab.make_set (map (fst o dest_TFree) type_args), Symtab.empty)
+         (Names.make_set (map (fst o dest_TFree) type_args), Names.empty)
          (Variable.maxidx_of lthy10 + 1);
 
     val ctr_post = delay_dummy_thm :: map (fn thm => thm RS @{thm sym}) ctrs_lazy_thms