changeset 62878 | 1cec457e0a03 |
parent 62821 | 48c24d0b6d85 |
child 62889 | 99c7f31615c2 |
--- a/src/Pure/Isar/runtime.ML Tue Apr 05 20:05:05 2016 +0200 +++ b/src/Pure/Isar/runtime.ML Tue Apr 05 20:51:37 2016 +0200 @@ -43,7 +43,7 @@ fun pretty_exn (exn: exn) = Pretty.from_ML (ML_Pretty.from_polyml - (ML_system_pretty (exn, FixedInt.fromInt (ML_Options.get_print_depth ())))); + (ML_system_pretty (exn, FixedInt.fromInt (ML_Print_Depth.get_print_depth ())))); (* exn_context *)