| changeset 45231 | d85a2fdc586c |
| parent 44794 | d3fdd0a24e15 |
| child 45294 | 3c5d3d286055 |
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy Fri Oct 21 11:17:12 2011 +0200 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Fri Oct 21 11:17:14 2011 +0200 @@ -495,7 +495,7 @@ lemma [code_post]: "raise' (STR s) = raise s" unfolding raise'_def by (simp add: STR_inverse) -lemma raise_raise' [code_inline]: +lemma raise_raise' [code_unfold]: "raise s = raise' (STR s)" unfolding raise'_def by (simp add: STR_inverse)