--- 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. *}