# HG changeset patch
# User wenzelm
# Date 1208278153 -7200
# Node ID 53e541e5b432bc7f61dd140e1ea3e50a4fd15067
# Parent  f978a6f489496322a4ea2ff73dd84953d957d575
Sign.hide_const;

diff -r f978a6f48949 -r 53e541e5b432 src/HOL/HOL.thy
--- 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}
 *}