# HG changeset patch
# User haftmann
# Date 1279118729 -7200
# Node ID 954c9ce1d3330e468af148d0c265fb09c4656cbc
# Parent  4c0a5e35931a18a7d75c1d82785341f7f1306258
repaired of_list implementation for SML, OCaml

diff -r 4c0a5e35931a -r 954c9ce1d333 src/HOL/Imperative_HOL/Array.thy
--- a/src/HOL/Imperative_HOL/Array.thy	Wed Jul 14 16:13:14 2010 +0200
+++ b/src/HOL/Imperative_HOL/Array.thy	Wed Jul 14 16:45:29 2010 +0200
@@ -451,7 +451,7 @@
 code_type array (SML "_/ array")
 code_const Array (SML "raise/ (Fail/ \"bare Array\")")
 code_const Array.new' (SML "(fn/ ()/ =>/ Array.array/ ((_),/ (_)))")
-code_const Array.of_list' (SML "(fn/ ()/ =>/ Array.fromList/ _)")
+code_const Array.of_list' (SML "((_); fn/ ()/ =>/ Array.fromList/ _)")
 code_const Array.make' (SML "(fn/ ()/ =>/ Array.tabulate/ ((_),/ (_)))")
 code_const Array.len' (SML "(fn/ ()/ =>/ Array.length/ _)")
 code_const Array.nth' (SML "(fn/ ()/ =>/ Array.sub/ ((_),/ (_)))")
@@ -465,7 +465,7 @@
 code_type array (OCaml "_/ array")
 code_const Array (OCaml "failwith/ \"bare Array\"")
 code_const Array.new' (OCaml "(fun/ ()/ ->/ Array.make/ (Big'_int.int'_of'_big'_int/ _)/ _)")
-code_const Array.of_list' (OCaml "(fun/ ()/ ->/ Array.of'_list/ _)")
+code_const Array.of_list' (OCaml "((_); fun/ ()/ ->/ Array.of'_list/ _)")
 code_const Array.len' (OCaml "(fun/ ()/ ->/ Big'_int.big'_int'_of'_int/ (Array.length/ _))")
 code_const Array.nth' (OCaml "(fun/ ()/ ->/ Array.get/ _/ (Big'_int.int'_of'_big'_int/ _))")
 code_const Array.upd' (OCaml "(fun/ ()/ ->/ Array.set/ _/ (Big'_int.int'_of'_big'_int/ _)/ _)")