1.1 --- a/src/HOL/RealDef.thy	Wed Dec 14 08:32:48 2011 +0100
     1.2 +++ b/src/HOL/RealDef.thy	Wed Dec 14 10:18:28 2011 +0100
     1.3 @@ -1767,7 +1767,7 @@
     1.4      (@{const_name uminus_real_inst.uminus_real}, @{const_name Nitpick.uminus_frac}),
     1.5      (@{const_name number_real_inst.number_of_real}, @{const_name Nitpick.number_of_frac}),
     1.6      (@{const_name inverse_real_inst.inverse_real}, @{const_name Nitpick.inverse_frac}),
     1.7 -    (@{const_name ord_real_inst.less_real}, @{const_name Nitpick.less_eq_frac}),
     1.8 +    (@{const_name ord_real_inst.less_real}, @{const_name Nitpick.less_frac}),
     1.9      (@{const_name ord_real_inst.less_eq_real}, @{const_name Nitpick.less_eq_frac})]
    1.10  *}
    1.11