src/Pure/ROOT.ML
changeset 62661 c23ff2f45a18
parent 62659 bb29cc00c31f
child 62662 291cc01f56f5
     1.1 --- a/src/Pure/ROOT.ML	Thu Mar 17 12:32:12 2016 +0100
     1.2 +++ b/src/Pure/ROOT.ML	Thu Mar 17 13:44:18 2016 +0100
     1.3 @@ -56,14 +56,6 @@
     1.4  
     1.5  use "ML/ml_pretty.ML";
     1.6  
     1.7 -local
     1.8 -  val depth = Unsynchronized.ref 10;
     1.9 -in
    1.10 -  fun get_default_print_depth () = ! depth;
    1.11 -  fun default_print_depth n = (depth := n; PolyML.print_depth n);
    1.12 -  val _ = default_print_depth 10;
    1.13 -end;
    1.14 -
    1.15  val error_depth = PolyML.error_depth;
    1.16  
    1.17