| 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;