| changeset 43948 | 8f5add916a99 |
| parent 42017 | 0d4bedb25fc9 |
| child 45030 | 9cf265a192f6 |
--- a/src/Pure/ML-Systems/proper_int.ML Sat Jul 23 16:37:17 2011 +0200 +++ b/src/Pure/ML-Systems/proper_int.ML Sat Jul 23 17:22:28 2011 +0200 @@ -5,8 +5,6 @@ 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;