
diff -r 2beb71c0f92e -r 8ef257366a0c src/HOL/Integ/NatBin.thy
--- a/src/HOL/Integ/NatBin.thy	Tue Sep 27 12:14:39 2005 +0200
+++ b/src/HOL/Integ/NatBin.thy	Tue Sep 27 12:16:06 2005 +0200
@@ -28,8 +28,6 @@
 lemma nat_number_of [simp]: "nat (number_of w) = number_of w"
 by (simp add: nat_number_of_def)
 
-declare nat_number_of [symmetric, THEN eq_reflection, code unfold]
-
 lemma nat_numeral_0_eq_0 [simp]: "Numeral0 = (0::nat)"
 by (simp add: nat_number_of_def)
 




