src/HOL/List.thy
changeset 36176 3fe7e97ccca8
parent 36154 11c6106d7787
child 36199 4d220994f30b
     1.1 --- a/src/HOL/List.thy	Fri Apr 16 20:56:40 2010 +0200
     1.2 +++ b/src/HOL/List.thy	Fri Apr 16 21:28:09 2010 +0200
     1.3 @@ -172,7 +172,8 @@
     1.4    insert :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
     1.5    "insert x xs = (if x \<in> set xs then xs else x # xs)"
     1.6  
     1.7 -hide (open) const insert hide (open) fact insert_def
     1.8 +hide_const (open) insert
     1.9 +hide_fact (open) insert_def
    1.10  
    1.11  primrec
    1.12    remove1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
    1.13 @@ -4584,7 +4585,7 @@
    1.14  
    1.15  declare set_map [symmetric, code_unfold]
    1.16  
    1.17 -hide (open) const length_unique
    1.18 +hide_const (open) length_unique
    1.19  
    1.20  
    1.21  text {* Code for bounded quantification and summation over nats. *}