# HG changeset patch
# User haftmann
# Date 1208972178 -7200
# Node ID f4cf7d36c63a2bfbbb155be620e08716f2e26fd1
# Parent  5a86bc79431ca6331eb1fb90749b6f88c8e5d12d
fixed proof

diff -r 5a86bc79431c -r f4cf7d36c63a 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 *}