src/Pure/ML/ml_pervasive.ML

--- a/src/Pure/ML/ml_pervasive.ML	Sat Apr 02 22:13:00 2016 +0200
+++ b/src/Pure/ML/ml_pervasive.ML	Sat Apr 02 22:38:26 2016 +0200
@@ -4,6 +4,12 @@
 Pervasive ML environment.
 *)
 
+structure PolyML_Pretty =
+struct
+  datatype context = datatype PolyML.context;
+  datatype pretty = datatype PolyML.pretty;
+end;
+
 val seconds = Time.fromReal;
 
 val _ =