src/HOL/Num.thy

--- a/src/HOL/Num.thy	Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/Num.thy	Sun Sep 13 22:56:52 2015 +0200
@@ -106,7 +106,7 @@
   "m < n \<longleftrightarrow> nat_of_num m < nat_of_num n"
 
 instance
-  by (default, auto simp add: less_num_def less_eq_num_def num_eq_iff)
+  by standard (auto simp add: less_num_def less_eq_num_def num_eq_iff)
 
 end