Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Function/induction_schema.ML
changeset 77879 dd222e2af01a
parent 74266 612b7e0d6721
child 79971 033f90dc441d 
--- 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
isabelle