--- a/src/HOL/Tools/Function/induction_schema.ML Fri Dec 17 16:25:21 2010 +0100
+++ b/src/HOL/Tools/Function/induction_schema.ML Fri Dec 17 17:08:56 2010 +0100
@@ -39,12 +39,12 @@
branches: scheme_branch list,
cases: scheme_case list}
-val ind_atomize = MetaSimplifier.rewrite true @{thms induct_atomize}
-val ind_rulify = MetaSimplifier.rewrite true @{thms induct_rulify}
+val ind_atomize = Raw_Simplifier.rewrite true @{thms induct_atomize}
+val ind_rulify = Raw_Simplifier.rewrite true @{thms induct_rulify}
fun meta thm = thm RS eq_reflection
-val sum_prod_conv = MetaSimplifier.rewrite true
+val sum_prod_conv = Raw_Simplifier.rewrite true
(map meta (@{thm split_conv} :: @{thms sum.cases}))
fun term_conv thy cv t =