src/HOL/Option.thy
changeset 36176 3fe7e97ccca8
parent 35719 99b6152aedf5
child 37880 3b9ca8d2c5fb
     1.1 --- a/src/HOL/Option.thy	Fri Apr 16 20:56:40 2010 +0200
     1.2 +++ b/src/HOL/Option.thy	Fri Apr 16 21:28:09 2010 +0200
     1.3 @@ -82,7 +82,7 @@
     1.4    by (rule ext) (simp split: sum.split)
     1.5  
     1.6  
     1.7 -hide (open) const set map
     1.8 +hide_const (open) set map
     1.9  
    1.10  subsubsection {* Code generator setup *}
    1.11  
    1.12 @@ -102,7 +102,7 @@
    1.13    "eq_class.eq x None \<longleftrightarrow> is_none x"
    1.14    by (simp add: eq is_none_none)
    1.15  
    1.16 -hide (open) const is_none
    1.17 +hide_const (open) is_none
    1.18  
    1.19  code_type option
    1.20    (SML "_ option")