src/HOL/Int.thy
changeset 36176 3fe7e97ccca8
parent 36076 882403378a41
child 36349 39be26d1bc28
--- a/src/HOL/Int.thy	Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Int.thy	Fri Apr 16 21:28:09 2010 +0200
@@ -2263,7 +2263,7 @@
 lemma [code]: "nat i = nat_aux i 0"
   by (simp add: nat_aux_def)
 
-hide (open) const nat_aux
+hide_const (open) nat_aux
 
 lemma zero_is_num_zero [code, code_unfold_post]:
   "(0\<Colon>int) = Numeral0" 
@@ -2325,7 +2325,7 @@
 
 quickcheck_params [default_type = int]
 
-hide (open) const Pls Min Bit0 Bit1 succ pred
+hide_const (open) Pls Min Bit0 Bit1 succ pred
 
 
 subsection {* Legacy theorems *}