src/HOL/Imperative_HOL/Heap_Monad.thy
changeset 36176 3fe7e97ccca8
parent 36078 59f6773a7d1d
child 37591 d3daea901123
     1.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Apr 16 20:56:40 2010 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Apr 16 21:28:09 2010 +0200
     1.3 @@ -405,7 +405,7 @@
     1.4  lemmas MREC_rule = mrec.MREC_rule
     1.5  lemmas MREC_pinduct = mrec.MREC_pinduct
     1.6  
     1.7 -hide (open) const heap execute
     1.8 +hide_const (open) heap execute
     1.9  
    1.10  
    1.11  subsection {* Code generator setup *}
    1.12 @@ -426,7 +426,7 @@
    1.13    "raise s = raise_exc (Fail (STR s))"
    1.14    unfolding Fail_def raise_exc_def raise_def ..
    1.15  
    1.16 -hide (open) const Fail raise_exc
    1.17 +hide_const (open) Fail raise_exc
    1.18  
    1.19  
    1.20  subsubsection {* SML and OCaml *}