| changeset 60731 | 4ac4b314d93c |
| parent 60729 | f5989a2c1f67 |
| child 60745 | d86b4cd0f1ec |
--- 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 *)