diff -r ed7d12bcf8f8 -r 108662d50512 src/HOL/Matrix/ComputeNumeral.thy
--- a/src/HOL/Matrix/ComputeNumeral.thy	Fri Feb 05 14:33:31 2010 +0100
+++ b/src/HOL/Matrix/ComputeNumeral.thy	Fri Feb 05 14:33:50 2010 +0100
@@ -109,22 +109,22 @@
 
 lemmas compute_natarith = bitarith natnorm natsuc natadd natsub natmul nateq natless natle natfac.simps
 
-lemma number_eq: "(((number_of x)::'a::{number_ring, ordered_idom}) = (number_of y)) = (x = y)"
+lemma number_eq: "(((number_of x)::'a::{number_ring, linordered_idom}) = (number_of y)) = (x = y)"
   unfolding number_of_eq
   apply simp
   done
 
-lemma number_le: "(((number_of x)::'a::{number_ring, ordered_idom}) \<le>  (number_of y)) = (x \<le> y)"
+lemma number_le: "(((number_of x)::'a::{number_ring, linordered_idom}) \<le>  (number_of y)) = (x \<le> y)"
   unfolding number_of_eq
   apply simp
   done
 
-lemma number_less: "(((number_of x)::'a::{number_ring, ordered_idom}) <  (number_of y)) = (x < y)"
+lemma number_less: "(((number_of x)::'a::{number_ring, linordered_idom}) <  (number_of y)) = (x < y)"
   unfolding number_of_eq 
   apply simp
   done
 
-lemma number_diff: "((number_of x)::'a::{number_ring, ordered_idom}) - number_of y = number_of (x + (- y))"
+lemma number_diff: "((number_of x)::'a::{number_ring, linordered_idom}) - number_of y = number_of (x + (- y))"
   apply (subst diff_number_of_eq)
   apply simp
   done