diff -r f6b0d827240e -r bdc1e2f0a86a src/HOL/Library/Code_Binary_Nat.thy --- a/src/HOL/Library/Code_Binary_Nat.thy Tue Sep 01 17:25:36 2015 +0200 +++ b/src/HOL/Library/Code_Binary_Nat.thy Tue Sep 01 22:32:58 2015 +0200 @@ -27,10 +27,10 @@ by (simp_all add: nat_of_num_inverse) lemma [code]: - "(1\nat) = Numeral1" + "(1::nat) = Numeral1" by simp -lemma [code_abbrev]: "Numeral1 = (1\nat)" +lemma [code_abbrev]: "Numeral1 = (1::nat)" by simp lemma [code]: