src/HOL/Real/RealOrd.ML

--- a/src/HOL/Real/RealOrd.ML	Wed May 10 21:04:16 2000 +0200
+++ b/src/HOL/Real/RealOrd.ML	Wed May 10 22:34:30 2000 +0200
@@ -812,7 +812,8 @@
 by (dtac lemma_nat_not_dense 1);
 by (auto_tac (claset(),
 	      simpset() addsimps [real_of_nat_Suc, real_of_nat_zero] @ 
-	                         real_add_ac));
+	                         real_add_ac
+                        delsimprocs Nat_Numeral_Simprocs.cancel_numerals));
 by (asm_full_simp_tac (simpset() addsimps [real_of_nat_one RS sym,
 					   real_of_nat_add,Suc_diff_n]) 1);
 qed "real_of_nat_minus";