--- 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")
--- 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 *}
--- 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 *}