src/HOL/Tools/Function/induction_schema.ML
changeset 55642 63beb38e9258
parent 54742 7a86358a3c0b
child 55968 94242fa87638
     1.1 --- a/src/HOL/Tools/Function/induction_schema.ML	Fri Feb 21 00:09:55 2014 +0100
     1.2 +++ b/src/HOL/Tools/Function/induction_schema.ML	Fri Feb 21 00:09:56 2014 +0100
     1.3 @@ -44,7 +44,7 @@
     1.4  fun meta thm = thm RS eq_reflection
     1.5  
     1.6  fun sum_prod_conv ctxt = Raw_Simplifier.rewrite ctxt true
     1.7 -  (map meta (@{thm split_conv} :: @{thms sum.cases}))
     1.8 +  (map meta (@{thm split_conv} :: @{thms sum.case}))
     1.9  
    1.10  fun term_conv thy cv t =
    1.11    cv (cterm_of thy t)
    1.12 @@ -315,7 +315,7 @@
    1.13          val Pxs = cert (HOLogic.mk_Trueprop (P_comp $ x))
    1.14            |> Goal.init
    1.15            |> (Simplifier.rewrite_goals_tac ctxt
    1.16 -                (map meta (branch_hyp :: @{thm split_conv} :: @{thms sum.cases}))
    1.17 +                (map meta (branch_hyp :: @{thm split_conv} :: @{thms sum.case}))
    1.18                THEN CONVERSION (ind_rulify ctxt) 1)
    1.19            |> Seq.hd
    1.20            |> Thm.elim_implies (Conv.fconv_rule Drule.beta_eta_conversion bstep)