--- a/src/HOL/Library/code_lazy.ML Wed Aug 25 22:17:38 2021 +0200
+++ b/src/HOL/Library/code_lazy.ML Thu Aug 26 14:45:19 2021 +0200
@@ -122,7 +122,7 @@
|> Conjunction.intr_balanced
|> rewrite_rule ctxt [Thm.symmetric (Thm.assume assum)]
|> Thm.implies_intr assum
- |> Thm.generalize ([], params) 0
+ |> Thm.generalize (Symtab.empty, Symtab.make_set params) 0
|> Axclass.unoverload ctxt
|> Thm.varifyT_global
end
@@ -494,7 +494,9 @@
val delay_dummy_thm = (pat_def_thm RS @{thm symmetric})
|> Drule.infer_instantiate' lthy10
[SOME (Thm.cterm_of lthy10 (Const (\<^const_name>\<open>Pure.dummy_pattern\<close>, HOLogic.unitT --> lazy_type)))]
- |> Thm.generalize (map (fst o dest_TFree) type_args, []) (Variable.maxidx_of lthy10 + 1);
+ |> Thm.generalize
+ (Symtab.make_set (map (fst o dest_TFree) type_args), Symtab.empty)
+ (Variable.maxidx_of lthy10 + 1);
val ctr_post = delay_dummy_thm :: map (fn thm => thm RS @{thm sym}) ctrs_lazy_thms
val ctr_thms_abs = map (fn thm => Drule.abs_def (thm RS @{thm eq_reflection})) ctrs_lazy_thms