src/HOL/Real/RComplete.thy

--- a/src/HOL/Real/RComplete.thy	Sun Jun 11 21:59:30 2006 +0200
+++ b/src/HOL/Real/RComplete.thy	Sun Jun 11 22:45:53 2006 +0200
@@ -1159,7 +1159,7 @@
 
 lemma natceiling_eq: "real n < x ==> x <= real n + 1 ==> natceiling x = n + 1"
   apply (unfold natceiling_def)
-  apply (subst nat_int [THEN sym]);back;
+  apply (simplesubst nat_int [THEN sym]) back back
   apply (subgoal_tac "nat(int n) + 1 = nat(int n + 1)")
   apply (erule ssubst)
   apply (subst eq_nat_nat_iff)