diff -r c4a27ab89c9b -r fdda3c18dbcd src/HOL/BNF/Examples/TreeFI.thy
--- a/src/HOL/BNF/Examples/TreeFI.thy	Thu Dec 13 09:21:45 2012 +0100
+++ b/src/HOL/BNF/Examples/TreeFI.thy	Thu Dec 13 12:48:45 2012 +0100
@@ -12,8 +12,6 @@
 imports ListF
 begin
 
-hide_const (open) Sublist.sub
-
 codata 'a treeFI = Tree (lab: 'a) (sub: "'a treeFI listF")
 
 lemma pre_treeFI_listF_set[simp]: "pre_treeFI_set2 (i, xs) = listF_set xs"