--- a/src/HOL/List.thy Fri Feb 14 07:53:46 2014 +0100
+++ b/src/HOL/List.thy Fri Feb 14 07:53:46 2014 +0100
@@ -34,6 +34,8 @@
setup {* Sign.parent_path *}
+hide_const (open) rel
+
syntax
-- {* list Enumeration *}
"_list" :: "args => 'a list" ("[(_)]")