--- a/src/HOL/Tools/function_package/induction_scheme.ML Thu Jun 26 10:07:01 2008 +0200
+++ b/src/HOL/Tools/function_package/induction_scheme.ML Thu Jun 26 11:58:27 2008 +0200
@@ -323,7 +323,7 @@
|> (MetaSimplifier.rewrite_goals_tac (map meta (branch_hyp :: @{thm split_conv} :: @{thms sum_cases}))
THEN CONVERSION ind_rulify 1)
|> Seq.hd
- |> Thm.elim_implies bstep
+ |> Thm.elim_implies (Conv.fconv_rule Drule.beta_eta_conversion bstep)
|> Goal.finish
|> implies_intr (cprop_of branch_hyp)
|> fold_rev (forall_intr o cert) fxs