src/HOL/Nat.thy

--- a/src/HOL/Nat.thy	Sat Mar 24 16:27:04 2012 +0100
+++ b/src/HOL/Nat.thy	Sun Mar 25 20:15:39 2012 +0200
@@ -181,7 +181,7 @@
 begin
 
 definition
-  One_nat_def [simp, code_post]: "1 = Suc 0"
+  One_nat_def [simp]: "1 = Suc 0"
 
 primrec times_nat where
   mult_0:     "0 * n = (0\<Colon>nat)"
@@ -1782,4 +1782,6 @@
 code_modulename Haskell
   Nat Arith
 
+hide_const (open) of_nat_aux
+
 end