diff -r 87f0f707a5f8 -r eeee8349e9eb src/Pure/ML-Systems/polyml.ML
--- a/src/Pure/ML-Systems/polyml.ML	Sun Aug 16 23:14:27 2015 +0200
+++ b/src/Pure/ML-Systems/polyml.ML	Mon Aug 17 15:19:25 2015 +0200
@@ -206,5 +206,6 @@
 
 (* ML debugger *)
 
-use "ML-Systems/ml_debugger.ML";
-if ML_System.name = "polyml-5.5.3" then use "ML-Systems/ml_debugger_polyml-5.5.3.ML" else ();
+if ML_System.name = "polyml-5.5.3"
+then use "ML-Systems/ml_debugger_polyml-5.5.3.ML"
+else use "ML-Systems/ml_debugger.ML";