src/HOL/Library/Code_Integer.thy
changeset 25767 852bce03412a
parent 24999 1dbe785ed529
child 25919 8b1c0d434824
--- 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