diff -r e30e51b7e4dc -r 0bd034a80a9a src/Pure/ML-Systems/polyml_common.ML
--- a/src/Pure/ML-Systems/polyml_common.ML	Fri Apr 16 10:15:00 2010 +0200
+++ b/src/Pure/ML-Systems/polyml_common.ML	Fri Apr 16 10:52:10 2010 +0200
@@ -55,7 +55,7 @@
 fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2);
 
 
-(* print depth *)
+(* toplevel printing *)
 
 local
   val depth = Unsynchronized.ref 10;
@@ -66,6 +66,8 @@
 
 val error_depth = PolyML.error_depth;
 
+val ml_make_string = "PolyML.makestring";
+
 
 
 (** interrupts **)