--- a/src/HOL/Library/Numeral_Type.thy Sat Jan 25 18:34:05 2014 +0100
+++ b/src/HOL/Library/Numeral_Type.thy Sat Jan 25 21:52:04 2014 +0100
@@ -284,8 +284,8 @@
lemmas bit0_iszero_numeral [simp] = bit0.iszero_numeral
lemmas bit1_iszero_numeral [simp] = bit1.iszero_numeral
-declare eq_numeral_iff_iszero [where 'a="('a::finite) bit0", standard, simp]
-declare eq_numeral_iff_iszero [where 'a="('a::finite) bit1", standard, simp]
+lemmas [simp] = eq_numeral_iff_iszero [where 'a="'a bit0"] for dummy :: "'a::finite"
+lemmas [simp] = eq_numeral_iff_iszero [where 'a="'a bit1"] for dummy :: "'a::finite"
subsection {* Order instances *}