--- a/src/HOL/Imperative_HOL/Heap_Monad.thy Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Fri Apr 16 21:28:09 2010 +0200
@@ -405,7 +405,7 @@
lemmas MREC_rule = mrec.MREC_rule
lemmas MREC_pinduct = mrec.MREC_pinduct
-hide (open) const heap execute
+hide_const (open) heap execute
subsection {* Code generator setup *}
@@ -426,7 +426,7 @@
"raise s = raise_exc (Fail (STR s))"
unfolding Fail_def raise_exc_def raise_def ..
-hide (open) const Fail raise_exc
+hide_const (open) Fail raise_exc
subsubsection {* SML and OCaml *}