no longer open PolyML -- to avoid surprises within the global name space;
recovered some important PolyML bindings (NB: print and makestring cannot be rebound without loosing infinite overloading);

--- a/src/Pure/ML-Systems/polyml_common.ML	Sun May 31 16:29:39 2009 +0200
+++ b/src/Pure/ML-Systems/polyml_common.ML	Sun May 31 16:41:52 2009 +0200
@@ -28,13 +28,7 @@
 
 (* old Poly/ML emulation *)
 
-local
-  val orig_exit = exit;
-in
-  open PolyML;
-  val exit = orig_exit;
-  fun quit () = exit 0;
-end;
+fun quit () = exit 0;
 
 
 (* restore old-style character / string functions *)
@@ -83,6 +77,8 @@
   fun print_depth n = (depth := n; PolyML.print_depth n);
 end;
 
+val error_depth = PolyML.error_depth;
+
 
 
 (** interrupts **)
@@ -134,7 +130,12 @@
   | SOME txt => txt);
 
 
-(* profile execution *)
+
+(** Runtime system **)
+
+val exception_trace = PolyML.exception_trace;
+val timing = PolyML.timing;
+val profiling = PolyML.profiling;
 
 fun profile 0 f x = f x
   | profile n f x =