src/HOL/Tools/Function/induction_schema.ML
changeset 41225 bd4ecd48c21f
parent 41117 d6379876ec4c
child 41228 e1fce873b814
     1.1 --- a/src/HOL/Tools/Function/induction_schema.ML	Fri Dec 17 13:12:58 2010 +0100
     1.2 +++ b/src/HOL/Tools/Function/induction_schema.ML	Fri Dec 17 13:45:43 2010 +0100
     1.3 @@ -312,7 +312,7 @@
     1.4  
     1.5          val Pxs = cert (HOLogic.mk_Trueprop (P_comp $ x))
     1.6            |> Goal.init
     1.7 -          |> (MetaSimplifier.rewrite_goals_tac (map meta (branch_hyp :: @{thm split_conv} :: @{thms sum.cases}))
     1.8 +          |> (Simplifier.rewrite_goals_tac (map meta (branch_hyp :: @{thm split_conv} :: @{thms sum.cases}))
     1.9                THEN CONVERSION ind_rulify 1)
    1.10            |> Seq.hd
    1.11            |> Thm.elim_implies (Conv.fconv_rule Drule.beta_eta_conversion bstep)