corrected setup for of_list
authorhaftmann
Sun Mar 21 06:59:23 2010 +0100 (2010-03-21)
changeset 358462ae4b7585501
parent 35845 e5980f0ad025
child 35847 19f1f7066917
child 35858 0d394a82337e
corrected setup for of_list
src/HOL/Imperative_HOL/Array.thy
     1.1 --- a/src/HOL/Imperative_HOL/Array.thy	Sat Mar 20 17:33:11 2010 +0100
     1.2 +++ b/src/HOL/Imperative_HOL/Array.thy	Sun Mar 21 06:59:23 2010 +0100
     1.3 @@ -163,7 +163,7 @@
     1.4  code_type array (SML "_/ array")
     1.5  code_const Array (SML "raise/ (Fail/ \"bare Array\")")
     1.6  code_const Array.new' (SML "(fn/ ()/ =>/ Array.array/ ((_),/ (_)))")
     1.7 -code_const Array.of_list (SML "(fn/ ()/ =>/ Array.fromList/ _)")
     1.8 +code_const Array.of_list' (SML "(fn/ ()/ =>/ Array.fromList/ _)")
     1.9  code_const Array.make' (SML "(fn/ ()/ =>/ Array.tabulate/ ((_),/ (_)))")
    1.10  code_const Array.length' (SML "(fn/ ()/ =>/ Array.length/ _)")
    1.11  code_const Array.nth' (SML "(fn/ ()/ =>/ Array.sub/ ((_),/ (_)))")
    1.12 @@ -177,7 +177,7 @@
    1.13  code_type array (OCaml "_/ array")
    1.14  code_const Array (OCaml "failwith/ \"bare Array\"")
    1.15  code_const Array.new' (OCaml "(fun/ ()/ ->/ Array.make/ (Big'_int.int'_of'_big'_int/ _)/ _)")
    1.16 -code_const Array.of_list (OCaml "(fun/ ()/ ->/ Array.of'_list/ _)")
    1.17 +code_const Array.of_list' (OCaml "(fun/ ()/ ->/ Array.of'_list/ _)")
    1.18  code_const Array.length' (OCaml "(fun/ ()/ ->/ Big'_int.big'_int'_of'_int/ (Array.length/ _))")
    1.19  code_const Array.nth' (OCaml "(fun/ ()/ ->/ Array.get/ _/ (Big'_int.int'_of'_big'_int/ _))")
    1.20  code_const Array.upd' (OCaml "(fun/ ()/ ->/ Array.set/ _/ (Big'_int.int'_of'_big'_int/ _)/ _)")