diff -r 8cd507be7138 -r 9d766f21cf41 src/HOL/Real/real_arith0.ML
--- a/src/HOL/Real/real_arith0.ML	Mon Jan 01 11:51:20 2001 +0100
+++ b/src/HOL/Real/real_arith0.ML	Mon Jan 01 11:52:04 2001 +0100
@@ -24,7 +24,7 @@
          real_mult_minus_1, real_mult_minus_1_right];
 
 val simprocs = [Real_Times_Assoc.conv, Real_Numeral_Simprocs.combine_numerals]@
-               Real_Numeral_Simprocs.cancel_numerals(* @ real_cancel_numeral_factors*);
+               Real_Numeral_Simprocs.cancel_numerals;
 
 val mono_ss = simpset() addsimps
                 [real_add_le_mono,real_add_less_mono,