--- a/src/HOL/Library/IArray.thy Wed Jan 28 08:29:08 2015 +0100
+++ b/src/HOL/Library/IArray.thy Wed Jan 28 08:29:08 2015 +0100
@@ -127,6 +127,16 @@
"IArray.length as = nat_of_integer (IArray.length' as)"
by simp
+context term_syntax
+begin
+
+lemma [code]:
+ "Code_Evaluation.term_of (as :: 'a::typerep iarray) =
+ Code_Evaluation.Const (STR ''IArray.iarray.IArray'') (TYPEREP('a list \<Rightarrow> 'a iarray)) <\<cdot>> (Code_Evaluation.term_of (IArray.list_of as))"
+ by (subst term_of_anything) rule
+
+end
+
code_printing
constant IArray.length' \<rightharpoonup> (SML) "Vector.length"