diff -r fdd6989cc8a0 -r 00f7618a9f2b src/Pure/ML/exn_output_polyml.ML
--- a/src/Pure/ML/exn_output_polyml.ML	Wed Feb 17 23:06:24 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,24 +0,0 @@
-(*  Title:      Pure/ML/exn_output_polyml.ML
-    Author:     Makarius
-
-Auxiliary operations for exception output -- Poly/ML version.
-*)
-
-signature EXN_OUTPUT =
-sig
-  val position: exn -> Position.T
-  val pretty: exn -> Pretty.T
-end;
-
-structure Exn_Output: EXN_OUTPUT =
-struct
-
-fun position exn =
-  (case PolyML.exceptionLocation exn of
-    NONE => Position.none
-  | SOME loc => Exn_Properties.position_of loc);
-
-fun pretty (exn: exn) =
-  Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (exn, ML_Options.get_print_depth ())));
-
-end;