# HG changeset patch
# User haftmann
# Date 1318769281 -7200
# Node ID 66e8a5812f413887f7e9be35c621f44287d8667a
# Parent  93e290c11b0ff3266fa13934b7de3de7dd2587e4
tuned proof

diff -r 93e290c11b0f -r 66e8a5812f41 src/HOL/ex/Numeral.thy
--- a/src/HOL/ex/Numeral.thy	Sun Oct 16 14:48:00 2011 +0200
+++ b/src/HOL/ex/Numeral.thy	Sun Oct 16 14:48:01 2011 +0200
@@ -893,7 +893,7 @@
 
 lemma one_int_code [code]:
   "1 = Pls One"
-  by (simp add: of_num_One)
+  by simp
 
 lemma plus_int_code [code]:
   "k + 0 = (k::int)"