--- a/src/HOL/Library/Code_Integer.thy Wed Jan 02 15:14:22 2008 +0100
+++ b/src/HOL/Library/Code_Integer.thy Wed Jan 02 15:14:23 2008 +0100
@@ -88,10 +88,10 @@
(OCaml "Big'_int.lt'_big'_int")
(Haskell infix 4 "<")
-code_const index_of_int and int_of_index
+(*code_const index_of_int and int_of_index
(SML "IntInf.toInt" and "IntInf.fromInt")
(OCaml "Big'_int.int'_of'_big'_int" and "Big'_int.big'_int'_of'_int")
- (Haskell "_" and "_")
+ (Haskell "_" and "_") FIXME perhaps recover this if neccessary *)
code_reserved SML IntInf
code_reserved OCaml Big_int