hide global sum

--- a/src/HOL/IMP/Hoare_Examples.thy	Mon Jan 09 15:54:48 2017 +0000
+++ b/src/HOL/IMP/Hoare_Examples.thy	Mon Jan 09 19:32:40 2017 +0100
@@ -2,6 +2,8 @@
 
 theory Hoare_Examples imports Hoare begin
 
+hide_const (open) sum
+
 text{* Summing up the first @{text x} natural numbers in variable @{text y}. *}
 
 fun sum :: "int \<Rightarrow> int" where