--- a/src/Pure/ML-Systems/smlnj.ML Tue Mar 25 17:59:34 2014 +0100
+++ b/src/Pure/ML-Systems/smlnj.ML Tue Mar 25 19:03:02 2014 +0100
@@ -56,11 +56,12 @@
local
val depth = ref (10: int);
in
- fun get_print_depth () = ! depth;
- fun print_depth n =
+ fun get_default_print_depth () = ! depth;
+ fun put_default_print_depth n =
(depth := n;
Control.Print.printDepth := dest_int n div 2;
Control.Print.printLength := dest_int n);
+ val _ = put_default_print_depth 10;
end;
val ml_make_string = "(fn _ => \"?\")";