# HG changeset patch
# User blanchet
# Date 1390238696 -3600
# Node ID b3e44be901227bf9ee98f17b5ccb2f35c6b2597e
# Parent  526671cca4a7997d713ee2af1ec9ba933f3c72f5
moved hide_const from BNF to Main

diff -r 526671cca4a7 -r b3e44be90122 src/HOL/BNF/BNF.thy
--- a/src/HOL/BNF/BNF.thy	Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/BNF/BNF.thy	Mon Jan 20 18:24:56 2014 +0100
@@ -13,8 +13,4 @@
 imports Countable_Set_Type BNF_Decl
 begin
 
-hide_const (open) image2 image2p vimage2p Gr Grp collect fsts snds setl setr 
-  convol pick_middlep fstOp sndOp csquare inver relImage relInvImage
-  prefCl PrefCl Succ Shift shift proj
-
 end
diff -r 526671cca4a7 -r b3e44be90122 src/HOL/Main.thy
--- a/src/HOL/Main.thy	Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/Main.thy	Mon Jan 20 18:24:56 2014 +0100
@@ -11,6 +11,11 @@
 
 text {* See further \cite{Nipkow-et-al:2002:tutorial} *}
 
+hide_const (open)
+  image2 image2p vimage2p Gr Grp collect fsts snds setl setr
+  convol pick_middlep fstOp sndOp csquare inver relImage relInvImage
+  prefCl PrefCl Succ Shift shift proj
+
 no_notation
   bot ("\<bottom>") and
   top ("\<top>") and