diff -r 6960410f134d -r 852bce03412a src/HOL/Library/Code_Integer.thy --- 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