# HG changeset patch
# User haftmann
# Date 1422430148 -3600
# Node ID c4f044389c283402ef7486ef641385cdbe3162b6
# Parent  180555df34ea53c21a602e5ca8017da939bc5135
proper term_of for iarray

diff -r 180555df34ea -r c4f044389c28 src/HOL/Library/IArray.thy
--- 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"