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 \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   "insert x xs = (if x \<in> 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 \<Rightarrow> 'a list \<Rightarrow> '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. *}