# HG changeset patch
# User haftmann
# Date 1486502104 -3600
# Node ID b316cd527a114eaec213264718b9c70a706fbc87
# Parent  a7af4045f873a9ea1d14f223c8069f1113834067
dropped superfluous preprocessing rule

diff -r a7af4045f873 -r b316cd527a11 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Tue Feb 07 22:15:03 2017 +0100
+++ b/src/HOL/Int.thy	Tue Feb 07 22:15:04 2017 +0100
@@ -1721,7 +1721,7 @@
 
 text \<open>Implementations.\<close>
 
-lemma one_int_code [code, code_unfold]: "1 = Pos Num.One"
+lemma one_int_code [code]: "1 = Pos Num.One"
   by simp
 
 lemma plus_int_code [code]: