diff -r a27b48967b26 -r 07dbdf60d5ad src/HOL/Tools/numeral_simprocs.ML
--- a/src/HOL/Tools/numeral_simprocs.ML	Mon Feb 08 14:22:22 2010 +0100
+++ b/src/HOL/Tools/numeral_simprocs.ML	Mon Feb 08 14:22:22 2010 +0100
@@ -581,11 +581,11 @@
      ["(l::'a::idom) * m = n",
       "(l::'a::idom) = m * n"],
      K EqCancelFactor.proc),
-    ("linlinordered_ring_le_cancel_factor",
+    ("linordered_ring_le_cancel_factor",
      ["(l::'a::linordered_ring) * m <= n",
       "(l::'a::linordered_ring) <= m * n"],
      K LeCancelFactor.proc),
-    ("linlinordered_ring_less_cancel_factor",
+    ("linordered_ring_less_cancel_factor",
      ["(l::'a::linordered_ring) * m < n",
       "(l::'a::linordered_ring) < m * n"],
      K LessCancelFactor.proc),