# HG changeset patch
# User wenzelm
# Date 1458332950 -3600
# Node ID b5c57430b9dd2431735af6663e2032c48a77cbf5
# Parent  068b430e678f0d92df5f256cdc76aeb983f2e676
observe ML print depth;

diff -r 068b430e678f -r b5c57430b9dd src/Pure/ML/ml_pp.ML
--- 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