--- a/src/Pure/ML-Systems/polyml.ML Thu Mar 27 13:00:40 2014 +0100
+++ b/src/Pure/ML-Systems/polyml.ML Thu Mar 27 17:12:40 2014 +0100
@@ -175,5 +175,5 @@
("PolyML.addPrettyPrinter (fn _ => fn _ => ml_pretty o Pretty.to_ML o (" ^ pp ^ "))");
val ml_make_string =
- "(fn x => Pretty.string_of (Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (x, ML_Compiler.get_print_depth ())))))";
+ "(fn x => Pretty.string_of (Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (x, ML_Options.get_print_depth ())))))";