src/HOL/Library/IArray.thy

--- a/src/HOL/Library/IArray.thy	Tue Sep 09 20:51:36 2014 +0200
+++ b/src/HOL/Library/IArray.thy	Tue Sep 09 20:51:36 2014 +0200
@@ -55,7 +55,7 @@
 | constant IArray.exists \<rightharpoonup> (SML) "Vector.exists"
 
 lemma [code]:
-"size (as :: 'a iarray) = 0"
+"size (as :: 'a iarray) = Suc (length (IArray.list_of as))"
 by (cases as) simp
 
 lemma [code]:
@@ -116,4 +116,3 @@
   constant IArray.length' \<rightharpoonup> (SML) "Vector.length"
 
 end
-