diff -r 0ea45a4d32f3 -r f2f1e50bf65d src/HOL/Tools/numeral_simprocs.ML
--- a/src/HOL/Tools/numeral_simprocs.ML	Mon Feb 08 11:01:47 2010 +0100
+++ b/src/HOL/Tools/numeral_simprocs.ML	Mon Feb 08 11:13:30 2010 +0100
@@ -255,20 +255,20 @@
       "(l::'a::number_ring) = m * n"],
      K EqCancelNumerals.proc),
     ("intless_cancel_numerals",
-     ["(l::'a::{ordered_idom,number_ring}) + m < n",
-      "(l::'a::{ordered_idom,number_ring}) < m + n",
-      "(l::'a::{ordered_idom,number_ring}) - m < n",
-      "(l::'a::{ordered_idom,number_ring}) < m - n",
-      "(l::'a::{ordered_idom,number_ring}) * m < n",
-      "(l::'a::{ordered_idom,number_ring}) < m * n"],
+     ["(l::'a::{linordered_idom,number_ring}) + m < n",
+      "(l::'a::{linordered_idom,number_ring}) < m + n",
+      "(l::'a::{linordered_idom,number_ring}) - m < n",
+      "(l::'a::{linordered_idom,number_ring}) < m - n",
+      "(l::'a::{linordered_idom,number_ring}) * m < n",
+      "(l::'a::{linordered_idom,number_ring}) < m * n"],
      K LessCancelNumerals.proc),
     ("intle_cancel_numerals",
-     ["(l::'a::{ordered_idom,number_ring}) + m <= n",
-      "(l::'a::{ordered_idom,number_ring}) <= m + n",
-      "(l::'a::{ordered_idom,number_ring}) - m <= n",
-      "(l::'a::{ordered_idom,number_ring}) <= m - n",
-      "(l::'a::{ordered_idom,number_ring}) * m <= n",
-      "(l::'a::{ordered_idom,number_ring}) <= m * n"],
+     ["(l::'a::{linordered_idom,number_ring}) + m <= n",
+      "(l::'a::{linordered_idom,number_ring}) <= m + n",
+      "(l::'a::{linordered_idom,number_ring}) - m <= n",
+      "(l::'a::{linordered_idom,number_ring}) <= m - n",
+      "(l::'a::{linordered_idom,number_ring}) * m <= n",
+      "(l::'a::{linordered_idom,number_ring}) <= m * n"],
      K LeCancelNumerals.proc)];
 
 structure CombineNumeralsData =
@@ -431,12 +431,12 @@
       "(l::'a::{idom,number_ring}) = m * n"],
      K EqCancelNumeralFactor.proc),
     ("ring_less_cancel_numeral_factor",
-     ["(l::'a::{ordered_idom,number_ring}) * m < n",
-      "(l::'a::{ordered_idom,number_ring}) < m * n"],
+     ["(l::'a::{linordered_idom,number_ring}) * m < n",
+      "(l::'a::{linordered_idom,number_ring}) < m * n"],
      K LessCancelNumeralFactor.proc),
     ("ring_le_cancel_numeral_factor",
-     ["(l::'a::{ordered_idom,number_ring}) * m <= n",
-      "(l::'a::{ordered_idom,number_ring}) <= m * n"],
+     ["(l::'a::{linordered_idom,number_ring}) * m <= n",
+      "(l::'a::{linordered_idom,number_ring}) <= m * n"],
      K LeCancelNumeralFactor.proc),
     ("int_div_cancel_numeral_factors",
      ["((l::'a::{semiring_div,number_ring}) * m) div n",
@@ -581,13 +581,13 @@
      ["(l::'a::idom) * m = n",
       "(l::'a::idom) = m * n"],
      K EqCancelFactor.proc),
-    ("ordered_ring_le_cancel_factor",
-     ["(l::'a::ordered_ring) * m <= n",
-      "(l::'a::ordered_ring) <= m * n"],
+    ("linlinordered_ring_le_cancel_factor",
+     ["(l::'a::linordered_ring) * m <= n",
+      "(l::'a::linordered_ring) <= m * n"],
      K LeCancelFactor.proc),
-    ("ordered_ring_less_cancel_factor",
-     ["(l::'a::ordered_ring) * m < n",
-      "(l::'a::ordered_ring) < m * n"],
+    ("linlinordered_ring_less_cancel_factor",
+     ["(l::'a::linordered_ring) * m < n",
+      "(l::'a::linordered_ring) < m * n"],
      K LessCancelFactor.proc),
     ("int_div_cancel_factor",
      ["((l::'a::semiring_div) * m) div n", "(l::'a::semiring_div) div (m * n)"],