# HG changeset patch
# User wenzelm
# Date 1279903366 -7200
# Node ID 94e9302a7fd014e69bbef770fa6a9c5ebf04f890
# Parent  844977c7abebe212e974d9d8f7aeb92ed33ab5f6# Parent  4b7afae88c576c270fc85317a30bf163c5dec1d7
merged

diff -r 4b7afae88c57 -r 94e9302a7fd0 src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy	Fri Jul 23 18:42:35 2010 +0200
+++ b/src/HOL/Code_Numeral.thy	Fri Jul 23 18:42:46 2010 +0200
@@ -298,7 +298,7 @@
 code_type code_numeral
   (SML "int")
   (OCaml "Big'_int.big'_int")
-  (Haskell "Int")
+  (Haskell "Integer")
   (Scala "Int")
 
 code_instance code_numeral :: eq
@@ -306,11 +306,9 @@
 
 setup {*
   fold (Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
-    false Code_Printer.literal_naive_numeral) ["SML", "Haskell"]
-  #> Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
-    false Code_Printer.literal_numeral "OCaml"
-  #> Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
-    false Code_Printer.literal_naive_numeral "Scala"
+    false Code_Printer.literal_naive_numeral) ["SML", "Scala"]
+  #> fold (Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
+    false Code_Printer.literal_numeral) ["OCaml", "Haskell"]
 *}
 
 code_reserved SML Int int
@@ -325,7 +323,7 @@
 code_const "subtract_code_numeral \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
   (SML "Int.max/ (_/ -/ _,/ 0 : int)")
   (OCaml "Big'_int.max'_big'_int/ (Big'_int.sub'_big'_int/ _/ _)/ Big'_int.zero'_big'_int")
-  (Haskell "max/ (_/ -/ _)/ (0 :: Int)")
+  (Haskell "max/ (_/ -/ _)/ (0 :: Integer)")
   (Scala "!(_/ -/ _).max(0)")
 
 code_const "op * \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
diff -r 4b7afae88c57 -r 94e9302a7fd0 src/HOL/Imperative_HOL/Heap_Monad.thy
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Jul 23 18:42:35 2010 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Jul 23 18:42:46 2010 +0200
@@ -433,28 +433,28 @@
 type RealWorld = Control.Monad.ST.RealWorld;
 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 Int a;
+type STArray s a = Data.Array.ST.STArray s Integer a;
 
 newSTRef = Data.STRef.newSTRef;
 readSTRef = Data.STRef.readSTRef;
 writeSTRef = Data.STRef.writeSTRef;
 
-newArray :: Int -> a -> ST s (STArray s a);
+newArray :: Integer -> a -> ST s (STArray s a);
 newArray k = Data.Array.ST.newArray (0, k);
 
 newListArray :: [a] -> ST s (STArray s a);
-newListArray xs = Data.Array.ST.newListArray (0, length xs) xs;
+newListArray xs = Data.Array.ST.newListArray (0, toInteger (length xs)) xs;
 
-newFunArray :: Int -> (Int -> a) -> ST s (STArray s a);
+newFunArray :: Integer -> (Integer -> a) -> ST s (STArray s a);
 newFunArray k f = Data.Array.ST.newListArray (0, k) (map f [0..k-1]);
 
-lengthArray :: STArray s a -> ST s Int;
+lengthArray :: STArray s a -> ST s Integer;
 lengthArray a = Control.Monad.liftM snd (Data.Array.ST.getBounds a);
 
-readArray :: STArray s a -> Int -> ST s a;
+readArray :: STArray s a -> Integer -> ST s a;
 readArray = Data.Array.ST.readArray;
 
-writeArray :: STArray s a -> Int -> a -> ST s ();
+writeArray :: STArray s a -> Integer -> a -> ST s ();
 writeArray = Data.Array.ST.writeArray;*}
 
 code_reserved Haskell Heap
diff -r 4b7afae88c57 -r 94e9302a7fd0 src/HOL/Library/Code_Integer.thy
--- a/src/HOL/Library/Code_Integer.thy	Fri Jul 23 18:42:35 2010 +0200
+++ b/src/HOL/Library/Code_Integer.thy	Fri Jul 23 18:42:46 2010 +0200
@@ -112,7 +112,7 @@
 code_const Code_Numeral.int_of
   (SML "IntInf.fromInt")
   (OCaml "_")
-  (Haskell "toEnum")
+  (Haskell "_")
   (Scala "!BigInt((_))")
 
 text {* Evaluation *}
diff -r 4b7afae88c57 -r 94e9302a7fd0 src/HOL/Library/Efficient_Nat.thy
--- a/src/HOL/Library/Efficient_Nat.thy	Fri Jul 23 18:42:35 2010 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy	Fri Jul 23 18:42:46 2010 +0200
@@ -412,13 +412,13 @@
 code_const Code_Numeral.of_nat
   (SML "IntInf.toInt")
   (OCaml "_")
-  (Haskell "fromEnum")
+  (Haskell "toInteger")
   (Scala "!_.as'_Int")
 
 code_const Code_Numeral.nat_of
   (SML "IntInf.fromInt")
   (OCaml "_")
-  (Haskell "toEnum")
+  (Haskell "fromInteger")
   (Scala "Nat")
 
 text {* Using target language arithmetic operations whenever appropriate *}
diff -r 4b7afae88c57 -r 94e9302a7fd0 src/HOL/Semiring_Normalization.thy
--- a/src/HOL/Semiring_Normalization.thy	Fri Jul 23 18:42:35 2010 +0200
+++ b/src/HOL/Semiring_Normalization.thy	Fri Jul 23 18:42:46 2010 +0200
@@ -36,7 +36,7 @@
 
 end
 
-sublocale idom < comm_semiring_1_cancel_crossproduct
+subclass (in idom) comm_semiring_1_cancel_crossproduct
 proof
   fix w x y z
   show "w * y + x * z = w * z + x * y \<longleftrightarrow> w = x \<or> y = z"
diff -r 4b7afae88c57 -r 94e9302a7fd0 src/Tools/Code/lib/Tools/codegen
--- a/src/Tools/Code/lib/Tools/codegen	Fri Jul 23 18:42:35 2010 +0200
+++ b/src/Tools/Code/lib/Tools/codegen	Fri Jul 23 18:42:46 2010 +0200
@@ -58,7 +58,7 @@
   QND_CMD="reset"
 fi
 
-CTXT_CMD="ML_Context.eval_text_in (SOME (ProofContext.init_global (theory \"HOL\"))) false Position.none \"Code_Target.shell_command thyname cmd\";"
+CTXT_CMD="ML_Context.eval_text_in (SOME (ProofContext.init_global (Thy_Info.get_theory \"HOL\"))) false Position.none \"Code_Target.shell_command thyname cmd\";"
 
 FULL_CMD="Unsynchronized.$QND_CMD quick_and_dirty; val thyname = \"$THY\"; val cmd = \"$CODE_CMD\"; $CTXT_CMD"