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 33697 7d6793ce0a26
parent 33471 5aef13872723
child 33855 cd8acf137c9c 
--- a/src/HOL/Tools/Function/induction_schema.ML	Sun Nov 15 15:14:02 2009 +0100
+++ b/src/HOL/Tools/Function/induction_schema.ML	Sun Nov 15 15:14:28 2009 +0100
@@ -383,7 +383,7 @@
 
     val res = Conjunction.intr_balanced (map_index project branches)
                  |> fold_rev implies_intr (map cprop_of newgoals @ steps)
-                 |> (fn thm => Thm.generalize ([], [Rn]) (Thm.maxidx_of thm + 1) thm)
+                 |> Drule.generalize ([], [Rn])
 
     val nbranches = length branches
     val npres = length pres
isabelle