diff -r 35a1788dd6f9 -r dd222e2af01a src/HOL/Tools/Function/induction_schema.ML
--- a/src/HOL/Tools/Function/induction_schema.ML	Tue Apr 18 21:47:40 2023 +0200
+++ b/src/HOL/Tools/Function/induction_schema.ML	Tue Apr 18 22:24:48 2023 +0200
@@ -381,7 +381,7 @@
 
     val res = Conjunction.intr_balanced (map_index project branches)
       |> fold_rev Thm.implies_intr (map Thm.cprop_of newgoals @ steps)
-      |> Drule.generalize (Names.empty, Names.make_set [Rn])
+      |> Drule.generalize (Names.empty, Names.make1_set Rn)
 
     val nbranches = length branches
     val npres = length pres