diff -r 2b97ea3130c2 -r 6b276119139b src/HOL/Library/Array.thy
--- a/src/HOL/Library/Array.thy	Sat Apr 26 13:20:16 2008 +0200
+++ b/src/HOL/Library/Array.thy	Sun Apr 27 17:13:01 2008 +0200
@@ -171,12 +171,12 @@
 
 code_type array (SML "_/ array")
 code_const Array (SML "raise/ (Fail/ \"bare Array\")")
-code_const Array.new' (SML "Array.array ((_), (_))")
-code_const Array.of_list (SML "Array.fromList")
-code_const Array.make' (SML "Array.tabulate ((_), (_))")
-code_const Array.length' (SML "Array.length")
-code_const Array.nth' (SML "Array.sub ((_), (_))")
-code_const Array.upd' (SML "Array.update ((_), (_), (_))")
+code_const Array.new' (SML "(fn/ ()/ =>/ Array.array/ ((_),/ (_)))")
+code_const Array.of_list (SML "(fn/ ()/ =>/ Array.fromList/ _)")
+code_const Array.make' (SML "(fn/ ()/ =>/ Array.tabulate/ ((_),/ (_)))")
+code_const Array.length' (SML "(fn/ ()/ =>/ Array.length/ _)")
+code_const Array.nth' (SML "(fn/ ()/ =>/ Array.sub/ ((_),/ (_)))")
+code_const Array.upd' (SML "(fn/ ()/ =>/ Array.update/ ((_),/ (_),/ (_)))")
 
 code_reserved SML Array
 
@@ -185,12 +185,12 @@
 
 code_type array (OCaml "_/ array")
 code_const Array (OCaml "failwith/ \"bare Array\"")
-code_const Array.new' (OCaml "Array.make")
-code_const Array.of_list (OCaml "Array.of_list")
-code_const Array.make' (OCaml "Array.init")
-code_const Array.length' (OCaml "Array.length")
-code_const Array.nth' (OCaml "Array.get")
-code_const Array.upd' (OCaml "Array.set")
+code_const Array.new' (OCaml "(fn/ ()/ =>/ Array.make/ _/ _)")
+code_const Array.of_list (OCaml "(fn/ ()/ =>/ Array.of'_list/ _)")
+code_const Array.make' (OCaml "(fn/ ()/ =>/ Array.init/ _/ _)")
+code_const Array.length' (OCaml "(fn/ ()/ =>/ Array.length/ _)")
+code_const Array.nth' (OCaml "(fn/ ()/ =>/ Array.get/ _/ _)")
+code_const Array.upd' (OCaml "(fn/ ()/ =>/ Array.set/ _/ _/ _)")
 
 code_reserved OCaml Array
 
@@ -205,5 +205,4 @@
 code_const Array.nth' (Haskell "readArray")
 code_const Array.upd' (Haskell "writeArray")
 
-
 end