# HG changeset patch
# User krauss
# Date 1214474307 -7200
# Node ID 7f242009f7b45dd2413e66e90c93a64cf113cefb
# Parent  9f90ac19e32bd7e8994c8f4aad3461b1b2179510
fix: need to beta/eta normalize

diff -r 9f90ac19e32b -r 7f242009f7b4 src/HOL/Tools/function_package/induction_scheme.ML
--- 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