diff -r 37745650a3f4 -r c9f374b64d99 src/HOL/Main.thy
--- a/src/HOL/Main.thy	Tue Sep 16 19:23:37 2014 +0200
+++ b/src/HOL/Main.thy	Tue Sep 16 19:23:37 2014 +0200
@@ -32,7 +32,9 @@
 hide_const (open)
   czero cinfinite cfinite csum cone ctwo Csum cprod cexp image2 image2p vimage2p Gr Grp collect
   fsts snds setl setr convol pick_middlep fstOp sndOp csquare relImage relInvImage Succ Shift
-  shift proj
+  shift proj id_bnf
+
+hide_fact (open) id_bnf_def type_definition_id_bnf_UNIV
 
 no_syntax (xsymbols)
   "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)