src/HOL/Imperative_HOL/Heap_Monad.thy
changeset 37591 d3daea901123
parent 36176 3fe7e97ccca8
child 37709 70fafefbcc98
     1.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Mon Jun 28 15:03:07 2010 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Mon Jun 28 15:03:07 2010 +0200
     1.3 @@ -379,7 +379,7 @@
     1.4          from this Inl 1(1) exec_f mrec show ?thesis
     1.5          proof (cases "ret_mrec")
     1.6            case (Inl aaa)
     1.7 -          from this mrec exec_f Inl' Inr' 1(1) mrec_rec 1(2)[OF exec_f Inl' Inr', of "aaa" "h2"] 1(3)
     1.8 +          from this mrec exec_f Inl' Inr' 1(1) mrec_rec 1(2) [OF exec_f [symmetric] Inl' Inr', of "aaa" "h2"] 1(3)
     1.9              show ?thesis
    1.10                apply auto
    1.11                apply (rule rec_case)