1.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Tue Jul 06 09:21:13 2010 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Tue Jul 06 09:21:13 2010 +0200
     1.3 @@ -349,8 +349,6 @@
     1.4  lemmas MREC_rule = mrec.MREC_rule
     1.5  lemmas MREC_pinduct = mrec.MREC_pinduct
     1.6  
     1.7 -hide_const (open) heap execute
     1.8 -
     1.9  
    1.10  subsection {* Code generator setup *}
    1.11  
    1.12 @@ -365,8 +363,6 @@
    1.13  
    1.14  code_datatype raise' -- {* avoid @{const "Heap"} formally *}
    1.15  
    1.16 -hide_const (open) raise'
    1.17 -
    1.18  
    1.19  subsubsection {* SML and OCaml *}
    1.20  
    1.21 @@ -493,4 +489,6 @@
    1.22  code_const return (Haskell "return")
    1.23  code_const Heap_Monad.raise' (Haskell "error/ _")
    1.24  
    1.25 +hide_const (open) Heap heap execute raise'
    1.26 +
    1.27  end