Sign.hide_const;
authorwenzelm
Tue, 15 Apr 2008 18:49:13 +0200 (2008-04-15)
changeset 26661 53e541e5b432
parent 26660 f978a6f48949
child 26662 39483503705f
Sign.hide_const;
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}
 *}