diff -r f1333a841b26 -r cbf2c5cf335e src/Pure/ML-Systems/proper_int.ML --- 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;