src/Pure/ML/ml_print_depth0.ML

--- a/src/Pure/ML/ml_print_depth0.ML	Thu Apr 07 13:35:08 2016 +0200
+++ b/src/Pure/ML/ml_print_depth0.ML	Thu Apr 07 13:54:02 2016 +0200
@@ -8,7 +8,6 @@
 sig
   val set_print_depth: int -> unit
   val get_print_depth: unit -> int
-  val get_print_depth_default: int -> int
 end;
 
 structure ML_Print_Depth: ML_PRINT_DEPTH =
@@ -18,6 +17,5 @@
 
 fun set_print_depth n = (depth := n; PolyML.print_depth n);
 fun get_print_depth () = ! depth;
-fun get_print_depth_default _ = ! depth;
 
 end;