observe ML print depth;

--- a/src/Pure/ML/ml_pp.ML	Fri Mar 18 21:21:09 2016 +0100
+++ b/src/Pure/ML/ml_pp.ML	Fri Mar 18 21:29:10 2016 +0100
@@ -8,24 +8,23 @@
 struct
 
 val _ =
-  PolyML.addPrettyPrinter
-    (fn _ => fn _ => Pretty.to_polyml o Proof_Display.pp_context);
+  PolyML.addPrettyPrinter (fn _ => fn _ => Pretty.to_polyml o Proof_Display.pp_context);
 
 val _ =
-  PolyML.addPrettyPrinter
-    (fn _ => fn _ => Pretty.to_polyml o Proof_Display.pp_thm Thy_Info.pure_theory);
+  PolyML.addPrettyPrinter (fn depth => fn _ =>
+    ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_thm Thy_Info.pure_theory);
 
 val _ =
-  PolyML.addPrettyPrinter
-    (fn _ => fn _ => Pretty.to_polyml o Proof_Display.pp_cterm Thy_Info.pure_theory);
+  PolyML.addPrettyPrinter (fn depth => fn _ =>
+    ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_cterm Thy_Info.pure_theory);
 
 val _ =
-  PolyML.addPrettyPrinter
-    (fn _ => fn _ => Pretty.to_polyml o Proof_Display.pp_ctyp Thy_Info.pure_theory);
+  PolyML.addPrettyPrinter (fn depth => fn _ =>
+    ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_ctyp Thy_Info.pure_theory);
 
 val _ =
-  PolyML.addPrettyPrinter
-    (fn _ => fn _ => Pretty.to_polyml o Proof_Display.pp_typ Thy_Info.pure_theory);
+  PolyML.addPrettyPrinter (fn depth => fn _ =>
+    ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_typ Thy_Info.pure_theory);
 
 
 local