src/Pure/pure_setup.ML

 then use "ML-Systems/install_pp_polyml-5.3.ML"
 else if String.isPrefix "polyml" ml_system
 then use "ML-Systems/install_pp_polyml.ML"
 else ();
 
+if ml_system = "polyml-5.0" orelse ml_system = "polyml-5.1" then
+  Secure.use_text ML_Parse.global_context (0, "") false
+    "PolyML.Compiler.maxInlineSize := 20"
+else ();
+
 
 (* ML toplevel use commands *)
 
 fun use name = Toplevel.program (fn () => ThyInfo.use name);
 fun use_thys name = Toplevel.program (fn () => ThyInfo.use_thys name);