workaround for strange compiler crash of Poly/ML 5.0 and 5.1 at this point http://isabelle.in.tum.de/repos/isabelle/file/a2fc533175ff/src/HOL/Tools/Nitpick/nitpick_nut.ML#l997
authorwenzelm
Sat, 28 Nov 2009 22:28:15 +0100
changeset 33917 186262d7cabf
parent 33916 a2fc533175ff
child 33918 5945e023bab7
workaround for strange compiler crash of Poly/ML 5.0 and 5.1 at this point http://isabelle.in.tum.de/repos/isabelle/file/a2fc533175ff/src/HOL/Tools/Nitpick/nitpick_nut.ML#l997
src/Pure/pure_setup.ML
--- a/src/Pure/pure_setup.ML	Sat Nov 28 20:03:07 2009 +0100
+++ b/src/Pure/pure_setup.ML	Sat Nov 28 22:28:15 2009 +0100
@@ -39,6 +39,11 @@
 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 *)