changeset 43948 | 8f5add916a99 |
parent 43703 | c37a1f29bbc0 |
--- a/src/Pure/ML-Systems/polyml_common.ML Sat Jul 23 16:37:17 2011 +0200 +++ b/src/Pure/ML-Systems/polyml_common.ML Sat Jul 23 17:22:28 2011 +0200 @@ -35,8 +35,6 @@ (* Compiler options *) -val ml_system_fix_ints = false; - PolyML.Compiler.printInAlphabeticalOrder := false; PolyML.Compiler.maxInlineSize := 80;