diff -r 02c2860fcf30 -r 4ac4b314d93c src/Pure/ML-Systems/polyml.ML
--- a/src/Pure/ML-Systems/polyml.ML	Thu Jul 16 11:38:18 2015 +0200
+++ b/src/Pure/ML-Systems/polyml.ML	Thu Jul 16 14:40:23 2015 +0200
@@ -132,6 +132,9 @@
 
 fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2);
 
+use "ML-Systems/ml_parse_tree.ML";
+if ML_System.name = "polyml-5.5.3" then use "ML-Systems/ml_parse_tree_polyml-5.5.3.ML" else ();
+
 
 (* ML debugger *)