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