src/HOL/Tools/Function/induction_schema.ML
changeset 33697 7d6793ce0a26
parent 33471 5aef13872723
child 33855 cd8acf137c9c
     1.1 --- a/src/HOL/Tools/Function/induction_schema.ML	Sun Nov 15 15:14:02 2009 +0100
     1.2 +++ b/src/HOL/Tools/Function/induction_schema.ML	Sun Nov 15 15:14:28 2009 +0100
     1.3 @@ -383,7 +383,7 @@
     1.4  
     1.5      val res = Conjunction.intr_balanced (map_index project branches)
     1.6                   |> fold_rev implies_intr (map cprop_of newgoals @ steps)
     1.7 -                 |> (fn thm => Thm.generalize ([], [Rn]) (Thm.maxidx_of thm + 1) thm)
     1.8 +                 |> Drule.generalize ([], [Rn])
     1.9  
    1.10      val nbranches = length branches
    1.11      val npres = length pres