src/HOL/Library/Array.thy

--- a/src/HOL/Library/Array.thy	Wed Apr 23 15:04:14 2008 +0200
+++ b/src/HOL/Library/Array.thy	Wed Apr 23 19:36:18 2008 +0200
@@ -164,8 +164,7 @@
 hide (open) const upd'
 lemma [code func]:
   "Array.upd i x a = Array.upd' a (index_of_nat i) x \<guillemotright> return a"
-  apply (simp add: upd'_def monad_simp)
-oops
+  by (simp add: upd'_def monad_simp upd_return)
 
 
 subsubsection {* SML *}