hide 'rel' name -- this one is waiting to be merged with 'list_all2'

--- 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"    ("[(_)]")