# HG changeset patch
# User haftmann
# Date 1216646784 -7200
# Node ID 52056ddac1942bfe93eaa31a08e75afcf46b6968
# Parent  558ceab467e15ba93aa90e361691f8dae6f0473d
fixed code generator setup

diff -r 558ceab467e1 -r 52056ddac194 src/HOL/Library/Array.thy
--- a/src/HOL/Library/Array.thy	Mon Jul 21 15:26:23 2008 +0200
+++ b/src/HOL/Library/Array.thy	Mon Jul 21 15:26:24 2008 +0200
@@ -186,12 +186,12 @@
 
 code_type array (OCaml "_/ array")
 code_const Array (OCaml "failwith/ \"bare Array\"")
-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_const Array.new' (OCaml "(fun/ ()/ ->/ Array.make/ _/ _)")
+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_reserved OCaml Array
 
@@ -202,7 +202,7 @@
 code_const Array (Haskell "error/ \"bare Array\"")
 code_const Array.new' (Haskell "newArray/ (0,/ _)")
 code_const Array.of_list' (Haskell "newListArray/ (0,/ _)")
-code_const Array.length' (Haskell "length")
+code_const Array.length' (Haskell "lengthArray")
 code_const Array.nth' (Haskell "readArray")
 code_const Array.upd' (Haskell "writeArray")
 
diff -r 558ceab467e1 -r 52056ddac194 src/HOL/Library/Efficient_Nat.thy
--- a/src/HOL/Library/Efficient_Nat.thy	Mon Jul 21 15:26:23 2008 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy	Mon Jul 21 15:26:24 2008 +0200
@@ -376,12 +376,12 @@
 code_const index_of_nat
   (SML "IntInf.toInt")
   (OCaml "Big'_int.int'_of'_big'_int")
-  (Haskell "toEnum")
+  (Haskell "fromEnum")
 
 code_const nat_of_index
   (SML "IntInf.fromInt")
   (OCaml "Big'_int.big'_int'_of'_int")
-  (Haskell "fromEnum")
+  (Haskell "toEnum")
 
 text {* Using target language arithmetic operations whenever appropriate *}
 
diff -r 558ceab467e1 -r 52056ddac194 src/HOL/Library/Heap_Monad.thy
--- a/src/HOL/Library/Heap_Monad.thy	Mon Jul 21 15:26:23 2008 +0200
+++ b/src/HOL/Library/Heap_Monad.thy	Mon Jul 21 15:26:24 2008 +0200
@@ -313,9 +313,9 @@
 code_const Heap (OCaml "failwith/ \"bare Heap\"")
 code_monad run "op \<guillemotright>=" return "()" OCaml
 code_const run (OCaml "_")
-code_const return (OCaml "(fn/ ()/ =>/ _)")
+code_const return (OCaml "(fun/ ()/ ->/ _)")
 code_const "Heap_Monad.Fail" (OCaml "Failure")
-code_const "Heap_Monad.raise_exc" (OCaml "(fn/ ()/ =>/ raise/ _)")
+code_const "Heap_Monad.raise_exc" (OCaml "(fun/ ()/ ->/ raise/ _)")
 
 code_reserved OCaml Failure raise
 
@@ -332,7 +332,7 @@
 
 type ST s a = Control.Monad.ST.ST s a;
 type STRef s a = Data.STRef.STRef s a;
-type STArray s a = Data.Array.ST.STArray s Integer a;
+type STArray s a = Data.Array.ST.STArray s Int a;
 
 runST :: (forall s. ST s a) -> a;
 runST s = Control.Monad.ST.runST s;
@@ -341,25 +341,25 @@
 readSTRef = Data.STRef.readSTRef;
 writeSTRef = Data.STRef.writeSTRef;
 
-newArray :: (Integer, Integer) -> a -> ST s (STArray s a);
+newArray :: (Int, Int) -> a -> ST s (STArray s a);
 newArray = Data.Array.ST.newArray;
 
-newListArray :: (Integer, Integer) -> [a] -> ST s (STArray s a);
+newListArray :: (Int, Int) -> [a] -> ST s (STArray s a);
 newListArray = Data.Array.ST.newListArray;
 
-length :: STArray s a -> ST s Integer;
-length a = Control.Monad.liftM snd (Data.Array.ST.getBounds a);
+lengthArray :: STArray s a -> ST s Int;
+lengthArray a = Control.Monad.liftM snd (Data.Array.ST.getBounds a);
 
-readArray :: STArray s a -> Integer -> ST s a;
+readArray :: STArray s a -> Int -> ST s a;
 readArray = Data.Array.ST.readArray;
 
-writeArray :: STArray s a -> Integer -> a -> ST s ();
+writeArray :: STArray s a -> Int -> a -> ST s ();
 writeArray = Data.Array.ST.writeArray;*}
 
 code_reserved Haskell ST STRef Array
   runST
   newSTRef reasSTRef writeSTRef
-  newArray newListArray bounds readArray writeArray
+  newArray newListArray lengthArray readArray writeArray
 
 text {* Monad *}