diff -r 56b6cdce22f1 -r 026f3db3f5c6 src/HOL/Real/rat_arith.ML
--- a/src/HOL/Real/rat_arith.ML	Wed Jun 11 18:02:00 2008 +0200
+++ b/src/HOL/Real/rat_arith.ML	Wed Jun 11 18:02:25 2008 +0200
@@ -13,7 +13,7 @@
 val simprocs = field_cancel_numeral_factors
 
 val simps = [@{thm order_less_irrefl}, @{thm neg_less_iff_less}, @{thm True_implies_equals},
-             inst "a" "(number_of ?v)" @{thm right_distrib},
+             OldGoals.inst "a" "(number_of ?v)" @{thm right_distrib},
              @{thm divide_1}, @{thm divide_zero_left},
              @{thm times_divide_eq_right}, @{thm times_divide_eq_left},
              @{thm minus_divide_left} RS sym, @{thm minus_divide_right} RS sym,