src/HOL/HOL.thy

--- a/src/HOL/HOL.thy	Tue May 04 08:55:39 2010 +0200
+++ b/src/HOL/HOL.thy	Tue May 04 08:55:43 2010 +0200
@@ -1886,7 +1886,6 @@
 *}
 
 hide_const (open) eq
-hide_const eq
 
 text {* Cases *}