--- a/src/HOL/Real/ferrante_rackoff.ML Thu Dec 07 21:44:13 2006 +0100
+++ b/src/HOL/Real/ferrante_rackoff.ML Thu Dec 07 23:16:55 2006 +0100
@@ -42,7 +42,7 @@
val powerarith =
map thm ["nat_number_of", "zpower_number_of_even",
"zpower_Pls", "zpower_Min"]
- @ [Tactic.simplify true [thm "zero_eq_Numeral0_nring", thm "one_eq_Numeral1_nring"]
+ @ [MetaSimplifier.simplify true [thm "zero_eq_Numeral0_nring", thm "one_eq_Numeral1_nring"]
(thm "zpower_number_of_odd")]
val comp_arith = binarith @ intarith @ intarithrel @ natarith