# HG changeset patch
# User wenzelm
# Date 1192288606 -7200
# Node ID 52eb78ebb370b9dc4c05e06c24aace7f6ac96843
# Parent  bb0dcb603a13ba907aeec114e24e06e778b6e1bd
PolyML.Compiler.maxInlineSize := 80;

diff -r bb0dcb603a13 -r 52eb78ebb370 src/Pure/ML-Systems/polyml.ML
--- 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 *)