src/Pure/ML-Systems/proper_int.ML
changeset 24597 cbf2c5cf335e
parent 24140 0683a2fc4041
child 24604 d5c5d2e13fbf
--- a/src/Pure/ML-Systems/proper_int.ML	Sun Sep 16 14:52:31 2007 +0200
+++ b/src/Pure/ML-Systems/proper_int.ML	Sun Sep 16 14:52:32 2007 +0200
@@ -6,6 +6,8 @@
 words.
 *)
 
+val ml_system_fix_ints = true;
+
 val mk_int = IntInf.fromInt: Int.int -> IntInf.int;
 val dest_int = IntInf.toInt: IntInf.int -> Int.int;