# HG changeset patch
# User haftmann
# Date 1283153863 -7200
# Node ID 8ffb9f5412859a030422ecc3c8fcc07cde78a822
# Parent  43c934dd4bc38d55f3e16ed4499356c9f54bd108
hide all-too-popular constant name eq

diff -r 43c934dd4bc3 -r 8ffb9f541285 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Mon Aug 30 09:35:30 2010 +0200
+++ b/src/HOL/HOL.thy	Mon Aug 30 09:37:43 2010 +0200
@@ -1875,8 +1875,6 @@
   Nbe.add_const_alias @{thm equal_alias_cert}
 *}
 
-hide_const (open) equal
-
 text {* Cases *}
 
 lemma Let_case_cert:
@@ -2127,4 +2125,6 @@
 
 *}
 
+hide_const (open) eq equal
+
 end