src/Pure/ML/ml_compiler0.ML

--- a/src/Pure/ML/ml_compiler0.ML	Sat Apr 02 20:33:34 2016 +0200
+++ b/src/Pure/ML/ml_compiler0.ML	Sat Apr 02 21:10:07 2016 +0200
@@ -139,3 +139,15 @@
         {verbose = true, debug = ML_Compiler0.debug_option opt_debug} file
       handle ERROR msg => (#print context msg; raise error "ML error"))
   end;
+
+
+(* export type-dependent functions *)
+
+ML_Compiler0.use_text
+  (ML_Compiler0.make_context
+    (ML_Name_Space.global_values
+      [("prettyRepresentation", "ML_system_pretty"),
+       ("addPrettyPrinter", "ML_system_pp"),
+       ("addOverload", "ML_system_overload")]))
+  {debug = false, file = "", line = 0, verbose = false}
+  "open PolyML RunCall";