diff -r 4c9e1e5a240e -r 4c232a2ddeab src/Pure/ML-Systems/ml_compiler_parameters_polyml-5.6.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/ml_compiler_parameters_polyml-5.6.ML	Sun Dec 06 23:10:08 2015 +0100
@@ -0,0 +1,12 @@
+(*  Title:      Pure/ML/ml_compiler_parameters_polyml-5.6.ML
+    Author:     Makarius
+
+Additional ML compiler parameters for Poly/ML 5.6, or later.
+*)
+
+structure ML_Compiler_Parameters: ML_COMPILER_PARAMETERS =
+struct
+
+fun debug b = [PolyML.Compiler.CPDebug b];
+
+end;
\ No newline at end of file