diff -r 831b3eb7ed8e -r 6607ccf77946 src/HOL/Imperative_HOL/Heap_Monad.thy
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Tue Jul 06 09:21:13 2010 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Tue Jul 06 09:21:13 2010 +0200
@@ -349,8 +349,6 @@
 lemmas MREC_rule = mrec.MREC_rule
 lemmas MREC_pinduct = mrec.MREC_pinduct
 
-hide_const (open) heap execute
-
 
 subsection {* Code generator setup *}
 
@@ -365,8 +363,6 @@
 
 code_datatype raise' -- {* avoid @{const "Heap"} formally *}
 
-hide_const (open) raise'
-
 
 subsubsection {* SML and OCaml *}
 
@@ -493,4 +489,6 @@
 code_const return (Haskell "return")
 code_const Heap_Monad.raise' (Haskell "error/ _")
 
+hide_const (open) Heap heap execute raise'
+
 end