src/HOL/Option.thy
changeset 36176 3fe7e97ccca8
parent 35719 99b6152aedf5
child 37880 3b9ca8d2c5fb
--- a/src/HOL/Option.thy	Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Option.thy	Fri Apr 16 21:28:09 2010 +0200
@@ -82,7 +82,7 @@
   by (rule ext) (simp split: sum.split)
 
 
-hide (open) const set map
+hide_const (open) set map
 
 subsubsection {* Code generator setup *}
 
@@ -102,7 +102,7 @@
   "eq_class.eq x None \<longleftrightarrow> is_none x"
   by (simp add: eq is_none_none)
 
-hide (open) const is_none
+hide_const (open) is_none
 
 code_type option
   (SML "_ option")