# HG changeset patch
# User haftmann
# Date 1253022083 -7200
# Node ID 5b88ae4307ff05fd3d78444941a4545f32c95940
# Parent  73ad5dbf1034b1cc373ae430e784d8dce3ae3e7b
restored code generation for OCaml

diff -r 73ad5dbf1034 -r 5b88ae4307ff src/HOL/Imperative_HOL/Array.thy
--- a/src/HOL/Imperative_HOL/Array.thy	Tue Sep 15 15:22:15 2009 +0200
+++ b/src/HOL/Imperative_HOL/Array.thy	Tue Sep 15 15:41:23 2009 +0200
@@ -176,12 +176,11 @@
 
 code_type array (OCaml "_/ array")
 code_const Array (OCaml "failwith/ \"bare Array\"")
-code_const Array.new' (OCaml "(fun/ ()/ ->/ Array.make/ _/ _)")
+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.make' (OCaml "(fun/ ()/ ->/ Array.init/ _/ _)")
-code_const Array.length' (OCaml "(fun/ ()/ ->/ Array.length/ _)")
-code_const Array.nth' (OCaml "(fun/ ()/ ->/ Array.get/ _/ _)")
-code_const Array.upd' (OCaml "(fun/ ()/ ->/ Array.set/ _/ _/ _)")
+code_const Array.length' (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/ _)/ _)")
 
 code_reserved OCaml Array
 
diff -r 73ad5dbf1034 -r 5b88ae4307ff src/HOL/Imperative_HOL/ex/Sublist.thy
--- a/src/HOL/Imperative_HOL/ex/Sublist.thy	Tue Sep 15 15:22:15 2009 +0200
+++ b/src/HOL/Imperative_HOL/ex/Sublist.thy	Tue Sep 15 15:41:23 2009 +0200
@@ -1,4 +1,3 @@
-(* $Id$ *)
 
 header {* Slices of lists *}
 
@@ -6,7 +5,6 @@
 imports Multiset
 begin
 
-
 lemma sublist_split: "i \<le> j \<and> j \<le> k \<Longrightarrow> sublist xs {i..<j} @ sublist xs {j..<k} = sublist xs {i..<k}" 
 apply (induct xs arbitrary: i j k)
 apply simp