# HG changeset patch
# User blanchet
# Date 1389903721 -3600
# Node ID 05cc0dbf3a5012e8f3a7815210d205e8f24e0c78
# Parent  38db7814481d745f0d4d8fe82da57cd6eaf7a187
hide short const name

diff -r 38db7814481d -r 05cc0dbf3a50 src/HOL/BNF/BNF.thy
--- a/src/HOL/BNF/BNF.thy	Thu Jan 16 20:52:54 2014 +0100
+++ b/src/HOL/BNF/BNF.thy	Thu Jan 16 21:22:01 2014 +0100
@@ -15,6 +15,6 @@
 
 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
+  prefCl PrefCl Succ Shift shift proj
 
 end
diff -r 38db7814481d -r 05cc0dbf3a50 src/HOL/BNF/BNF_GFP.thy
--- a/src/HOL/BNF/BNF_GFP.thy	Thu Jan 16 20:52:54 2014 +0100
+++ b/src/HOL/BNF/BNF_GFP.thy	Thu Jan 16 21:22:01 2014 +0100
@@ -15,6 +15,10 @@
   "primcorec" :: thy_decl
 begin
 
+setup {*
+Sign.const_alias @{binding proj} @{const_name Equiv_Relations.proj}
+*}
+
 lemma not_TrueE: "\<not> True \<Longrightarrow> P"
 by (erule notE, rule TrueI)
 
diff -r 38db7814481d -r 05cc0dbf3a50 src/HOL/Equiv_Relations.thy
--- a/src/HOL/Equiv_Relations.thy	Thu Jan 16 20:52:54 2014 +0100
+++ b/src/HOL/Equiv_Relations.thy	Thu Jan 16 21:22:01 2014 +0100
@@ -497,5 +497,6 @@
   "equivp R \<Longrightarrow> R x y \<Longrightarrow> R y z \<Longrightarrow> R x z"
   by (erule equivpE, erule transpE)
 
+hide_const (open) proj
+
 end
-