hide successor

--- a/src/HOL/List.thy	Mon Sep 24 22:00:18 2007 +0200
+++ b/src/HOL/List.thy	Tue Sep 25 10:27:43 2007 +0200
@@ -2596,6 +2596,8 @@
 
 text{* Now @{term"[i..j::int]"} is defined for integers. *}
 
+hide (open) const successor
+
 
 subsubsection {* @{text lists}: the list-forming operator over sets *}