--- a/src/HOL/HOL.thy Tue Apr 15 18:49:12 2008 +0200
+++ b/src/HOL/HOL.thy Tue Apr 15 18:49:13 2008 +0200
@@ -1695,7 +1695,7 @@
end
setup {*
- Sign.hide_names_i true ("const", ["HOL.eq"])
+ Sign.hide_const true "HOL.eq"
#> CodeUnit.add_const_alias @{thm equals_eq}
*}