src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML

--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Wed Aug 25 22:17:38 2021 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Thu Aug 26 14:45:19 2021 +0200
@@ -160,7 +160,7 @@
       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 ([], [s])
+      |> Drule.generalize (Symtab.empty, Symtab.make_set [s])
     end
   | _ => split);