| changeset 30619 | 0226c07352db |
| parent 30187 | b92b3375e919 |
| child 30625 | d53d1a16d5ee |
--- a/src/Pure/ML-Systems/mosml.ML Sat Mar 21 13:11:12 2009 +0100 +++ b/src/Pure/ML-Systems/mosml.ML Sat Mar 21 15:08:00 2009 +0100 @@ -45,6 +45,7 @@ use "ML-Systems/multithreading.ML"; use "ML-Systems/time_limit.ML"; use "ML-Systems/ml_name_space.ML"; +use "ML-Systems/ml_pretty.ML"; (*low-level pointer equality*)