# HG changeset patch
# User haftmann
# Date 1278400873 -7200
# Node ID 6607ccf779467cd0110099bbac2a97d2ebdc900c
# Parent  831b3eb7ed8e7cb0c4c47a1e8fe645e2d4e95a2b
tuned

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