src/HOL/Nat.thy

--- a/src/HOL/Nat.thy	Wed Feb 14 10:06:13 2007 +0100
+++ b/src/HOL/Nat.thy	Wed Feb 14 10:06:14 2007 +0100
@@ -439,7 +439,7 @@
 
 text {* Type {@typ nat} is a wellfounded linear order *}
 
-instance nat :: "{order, linorder, wellorder}"
+instance nat :: wellorder
   by intro_classes
     (assumption |
       rule le_refl le_trans le_anti_sym nat_less_le nat_le_linear wf_less)+