--- 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