src/HOL/Tools/Function/induction_schema.ML
changeset 41228 e1fce873b814
parent 41225 bd4ecd48c21f
child 41418 b6dc60638be0
     1.1 --- a/src/HOL/Tools/Function/induction_schema.ML	Fri Dec 17 16:25:21 2010 +0100
     1.2 +++ b/src/HOL/Tools/Function/induction_schema.ML	Fri Dec 17 17:08:56 2010 +0100
     1.3 @@ -39,12 +39,12 @@
     1.4    branches: scheme_branch list,
     1.5    cases: scheme_case list}
     1.6  
     1.7 -val ind_atomize = MetaSimplifier.rewrite true @{thms induct_atomize}
     1.8 -val ind_rulify = MetaSimplifier.rewrite true @{thms induct_rulify}
     1.9 +val ind_atomize = Raw_Simplifier.rewrite true @{thms induct_atomize}
    1.10 +val ind_rulify = Raw_Simplifier.rewrite true @{thms induct_rulify}
    1.11  
    1.12  fun meta thm = thm RS eq_reflection
    1.13  
    1.14 -val sum_prod_conv = MetaSimplifier.rewrite true
    1.15 +val sum_prod_conv = Raw_Simplifier.rewrite true
    1.16    (map meta (@{thm split_conv} :: @{thms sum.cases}))
    1.17  
    1.18  fun term_conv thy cv t =