| changeset 30619 | 0226c07352db |
| parent 30187 | b92b3375e919 |
| child 30625 | d53d1a16d5ee |
--- a/src/Pure/ML-Systems/polyml_common.ML Sat Mar 21 13:11:12 2009 +0100 +++ b/src/Pure/ML-Systems/polyml_common.ML Sat Mar 21 15:08:00 2009 +0100 @@ -10,6 +10,7 @@ use "ML-Systems/time_limit.ML"; use "ML-Systems/system_shell.ML"; use "ML-Systems/ml_name_space.ML"; +use "ML-Systems/ml_pretty.ML"; (** ML system and platform related **)