diff -r 5cec4ca719d1 -r 3fe7e97ccca8 src/HOL/List.thy --- a/src/HOL/List.thy Fri Apr 16 20:56:40 2010 +0200 +++ b/src/HOL/List.thy Fri Apr 16 21:28:09 2010 +0200 @@ -172,7 +172,8 @@ insert :: "'a \ 'a list \ 'a list" where "insert x xs = (if x \ set xs then xs else x # xs)" -hide (open) const insert hide (open) fact insert_def +hide_const (open) insert +hide_fact (open) insert_def primrec remove1 :: "'a \ 'a list \ 'a list" where @@ -4584,7 +4585,7 @@ declare set_map [symmetric, code_unfold] -hide (open) const length_unique +hide_const (open) length_unique text {* Code for bounded quantification and summation over nats. *}