diff -r ed7d12bcf8f8 -r 108662d50512 src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy	Fri Feb 05 14:33:31 2010 +0100
+++ b/src/HOL/Code_Numeral.thy	Fri Feb 05 14:33:50 2010 +0100
@@ -144,7 +144,7 @@
 
 subsection {* Basic arithmetic *}
 
-instantiation code_numeral :: "{minus, ordered_semidom, semiring_div, linorder}"
+instantiation code_numeral :: "{minus, linordered_semidom, semiring_div, linorder}"
 begin
 
 definition [simp, code del]: