author | wenzelm |
Sat, 13 Oct 2007 17:16:46 +0200 | |
changeset 25023 | 52eb78ebb370 |
parent 25022 | bb0dcb603a13 |
child 25024 | 0615bb9955dd |
--- a/src/Pure/ML-Systems/polyml.ML Sat Oct 13 17:16:45 2007 +0200 +++ b/src/Pure/ML-Systems/polyml.ML Sat Oct 13 17:16:46 2007 +0200 @@ -8,10 +8,13 @@ use "ML-Systems/multithreading.ML"; use "ML-Systems/time_limit.ML"; + +(** ML system and platform related **) + val ml_system_fix_ints = false; +PolyML.Compiler.maxInlineSize := 80; -(** ML system and platform related **) (* String compatibility *)