src/HOL/Library/Numeral_Type.thy

--- a/src/HOL/Library/Numeral_Type.thy	Mon Jul 06 22:06:02 2015 +0200
+++ b/src/HOL/Library/Numeral_Type.thy	Mon Jul 06 22:57:34 2015 +0200
@@ -192,8 +192,8 @@
 lemma num1_eq_iff: "(x::num1) = (y::num1) \<longleftrightarrow> True"
   by (induct x, induct y) simp
 
-instance proof
-qed (simp_all add: num1_eq_iff)
+instance
+  by standard (simp_all add: num1_eq_iff)
 
 end