--- a/src/Pure/ML/ml_print_depth.ML Thu Apr 07 13:35:08 2016 +0200
+++ b/src/Pure/ML/ml_print_depth.ML Thu Apr 07 13:54:02 2016 +0200
@@ -10,7 +10,6 @@
val print_depth_raw: Config.raw
val print_depth: int Config.T
val get_print_depth: unit -> int
- val get_print_depth_default: int -> int
end;
structure ML_Print_Depth: ML_PRINT_DEPTH =
@@ -29,9 +28,4 @@
NONE => ML_Print_Depth.get_print_depth ()
| SOME context => Config.get_generic context print_depth);
-fun get_print_depth_default default =
- (case Context.get_generic_context () of
- NONE => default
- | SOME context => Config.get_generic context print_depth);
-
end;