--- 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} *}