diff -r cbb94074682b -r 6646bb548c6b src/HOL/Library/IArray.thy
--- a/src/HOL/Library/IArray.thy	Sun Jun 23 21:16:06 2013 +0200
+++ b/src/HOL/Library/IArray.thy	Sun Jun 23 21:16:07 2013 +0200
@@ -40,11 +40,9 @@
 
 code_reserved SML Vector
 
-code_type iarray
-  (SML "_ Vector.vector")
-
-code_const IArray
-  (SML "Vector.fromList")
+code_printing
+  type_constructor iarray \<rightharpoonup> (SML) "_ Vector.vector"
+| constant IArray \<rightharpoonup> (SML) "Vector.fromList"
 
 lemma [code]:
 "size (as :: 'a iarray) = 0"
@@ -74,8 +72,8 @@
 "IArray.of_fun f n = IArray.tabulate (integer_of_nat n, f \<circ> nat_of_integer)"
 by simp 
 
-code_const IArray.tabulate
-  (SML "Vector.tabulate")
+code_printing
+  constant IArray.tabulate \<rightharpoonup> (SML) "Vector.tabulate"
 
 primrec sub' :: "'a iarray \<times> integer \<Rightarrow> 'a" where
 "sub' (as, n) = IArray.list_of as ! nat_of_integer n"
@@ -85,8 +83,8 @@
 "as !! n = IArray.sub' (as, integer_of_nat n)"
 by simp
 
-code_const IArray.sub'
-  (SML "Vector.sub")
+code_printing
+  constant IArray.sub' \<rightharpoonup> (SML) "Vector.sub"
 
 definition length' :: "'a iarray \<Rightarrow> integer" where
 [simp]: "length' as = integer_of_nat (List.length (IArray.list_of as))"
@@ -96,8 +94,8 @@
 "IArray.length as = nat_of_integer (IArray.length' as)"
 by simp
 
-code_const IArray.length'
-  (SML "Vector.length")
+code_printing
+  constant IArray.length' \<rightharpoonup> (SML) "Vector.length"
 
 end