diff -r 5cec4ca719d1 -r 3fe7e97ccca8 src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy	Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Code_Numeral.thy	Fri Apr 16 21:28:09 2010 +0200
@@ -278,7 +278,7 @@
   then show ?thesis by (auto simp add: int_of_def mult_ac)
 qed
 
-hide (open) const of_nat nat_of int_of
+hide_const (open) of_nat nat_of int_of
 
 subsubsection {* Lazy Evaluation of an indexed function *}
 
@@ -289,7 +289,7 @@
 
 termination by (relation "measure (%(f, n, m). Code_Numeral.nat_of (m + 1 - n))") auto
 
-hide (open) const iterate_upto
+hide_const (open) iterate_upto
 
 subsection {* Code generator setup *}