src/HOL/Code_Numeral.thy

   then have "int (nat_of k) = int (nat_of k div 2) * 2 + int (nat_of k mod 2)" 
     unfolding int_mult zadd_int [symmetric] by simp
   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 *}
 
 function iterate_upto :: "(code_numeral => 'a) => code_numeral => code_numeral => 'a Predicate.pred"
 where
   "iterate_upto f n m = Predicate.Seq (%u. if n > m then Predicate.Empty else Predicate.Insert (f n) (iterate_upto f (n + 1) m))"
 by pat_completeness auto
 
 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 *}
 
 text {* Implementation of indices by bounded integers *}