--- a/src/HOL/HOL.thy Mon Aug 30 09:35:30 2010 +0200 +++ b/src/HOL/HOL.thy Mon Aug 30 09:37:43 2010 +0200 @@ -1875,8 +1875,6 @@ Nbe.add_const_alias @{thm equal_alias_cert} *} -hide_const (open) equal - text {* Cases *} lemma Let_case_cert: @@ -2127,4 +2125,6 @@ *} +hide_const (open) eq equal + end