--- 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