diff -r 0c652e82fdf4 -r a259d259c797 src/HOL/Library/Array.thy
--- a/src/HOL/Library/Array.thy	Thu Apr 17 22:28:56 2008 +0200
+++ b/src/HOL/Library/Array.thy	Fri Apr 18 09:44:16 2008 +0200
@@ -46,14 +46,19 @@
 where
   [code del]: "upd i x a = (do len \<leftarrow> length a;
                       (if i < len
-                           then Heap_Monad.heap (\<lambda>h. ((), Heap.upd a i x h))
-                           else raise (''array update: index out of range''));
-                      return a
+                           then Heap_Monad.heap (\<lambda>h. (a, Heap.upd a i x h))
+                           else raise (''array update: index out of range''))
                    done)" 
 
 lemma upd_return:
   "upd i x a \<guillemotright> return a = upd i x a"
-  unfolding upd_def by (simp add: monad_simp)
+proof (rule Heap_eqI)
+  fix h
+  obtain len h' where "Heap_Monad.execute (Array.length a) h = (len, h')"
+    by (cases "Heap_Monad.execute (Array.length a) h")
+  then show "Heap_Monad.execute (upd i x a \<guillemotright> return a) h = Heap_Monad.execute (upd i x a) h"
+    by (auto simp add: upd_def bindM_def run_drop split: sum.split)
+qed
 
 
 subsection {* Derivates *}
@@ -159,7 +164,8 @@
 hide (open) const upd'
 lemma [code func]:
   "Array.upd i x a = Array.upd' a (index_of_nat i) x \<guillemotright> return a"
-  by (simp add: upd'_def monad_simp upd_return)
+  apply (simp add: upd'_def monad_simp)
+oops
 
 
 subsubsection {* SML *}