diff -r fac0c76bbda2 -r af71b753c459 src/HOL/BNF/BNF.thy
--- a/src/HOL/BNF/BNF.thy	Fri Dec 20 21:09:01 2013 +0100
+++ b/src/HOL/BNF/BNF.thy	Wed Dec 18 11:03:40 2013 +0100
@@ -14,7 +14,7 @@
 begin
 
 hide_const (open) image2 image2p vimage2p Gr Grp collect fsts snds setl setr 
-  convol thePull pick_middlep fstOp sndOp csquare inver
-  image2 relImage relInvImage prefCl PrefCl Succ Shift shift
+  convol pick_middlep fstOp sndOp csquare inver relImage relInvImage
+  prefCl PrefCl Succ Shift shift
 
 end