src/HOL/Tools/BNF/bnf_fp_def_sugar.ML

                 |> infer_instantiate' lthy (replicate live NONE @
                   [SOME (Thm.cterm_of lthy (ctorA $ y))])
                 |> unfold_thms lthy [dtor_ctor];
             in
               (fp_map_thm' RS ctor_cong RS (ctor_dtor RS sym RS trans))
-              |> Drule.generalize ([], [y_s])
+              |> Drule.generalize (Symtab.empty, Symtab.make_set [y_s])
             end;
 
         val map_thms =
           let
             fun mk_goal ctrA ctrB xs ys =

             in
               fp_rel_thm
               |> infer_instantiate' lthy (replicate live NONE @
                 [SOME (Thm.cterm_of lthy (ctorA $ y)), SOME (Thm.cterm_of lthy (ctorB $ z))])
               |> unfold_thms lthy [dtor_ctor]
-              |> Drule.generalize ([], [y_s, z_s])
+              |> Drule.generalize (Symtab.empty, Symtab.make_set [y_s, z_s])
             end;
 
         val rel_inject_thms =
           let
             fun mk_goal ctrA ctrB xs ys =