src/HOL/HOL.thy

--- a/src/HOL/HOL.thy	Tue Apr 22 08:33:13 2008 +0200
+++ b/src/HOL/HOL.thy	Tue Apr 22 08:33:16 2008 +0200
@@ -1694,9 +1694,11 @@
 
 end
 
+hide (open) const eq
+hide const eq
+
 setup {*
-  Sign.hide_const true "HOL.eq"
-  #> CodeUnit.add_const_alias @{thm equals_eq}
+  CodeUnit.add_const_alias @{thm equals_eq}
 *}
 
 lemma [code func]: