src/HOL/Imperative_HOL/Heap_Monad.thy

 
 abbreviation "MREC == mrec.MREC"
 lemmas MREC_rule = mrec.MREC_rule
 lemmas MREC_pinduct = mrec.MREC_pinduct
 
-hide_const (open) heap execute
-
 
 subsection {* Code generator setup *}
 
 subsubsection {* Logical intermediate layer *}
 

 lemma raise_raise' [code_inline]:
   "raise s = raise' (STR s)"
   by simp
 
 code_datatype raise' -- {* avoid @{const "Heap"} formally *}
-
-hide_const (open) raise'
 
 
 subsubsection {* SML and OCaml *}
 
 code_type Heap (SML "unit/ ->/ _")

 code_type Heap (Haskell "Heap.ST/ Heap.RealWorld/ _")
 code_monad "op \<guillemotright>=" Haskell
 code_const return (Haskell "return")
 code_const Heap_Monad.raise' (Haskell "error/ _")
 
+hide_const (open) Heap heap execute raise'
+
 end