src/Pure/ML-Systems/polyml.ML
changeset 50911 ee7fe4230642
parent 50910 54f06ba192ef
child 51638 1275716f395b
--- a/src/Pure/ML-Systems/polyml.ML	Wed Jan 16 11:31:08 2013 +0100
+++ b/src/Pure/ML-Systems/polyml.ML	Wed Jan 16 16:26:36 2013 +0100
@@ -11,22 +11,6 @@
     NONE => raise exn
   | SOME location => PolyML.raiseWithLocation (exn, location));
 
-fun set_exn_serial i exn = (*requires uninterruptible*)
-  let
-    val (file, startLine, endLine) =
-      (case PolyML.exceptionLocation exn of
-        NONE => ("", 0, 0)
-      | SOME {file, startLine, endLine, startPosition, ...} => (file, startLine, endLine));
-    val location =
-      {file = file, startLine = startLine, endLine = endLine,
-        startPosition = ~ i, endPosition = 0};
-  in PolyML.raiseWithLocation (exn, location) handle e => e end;
-
-fun get_exn_serial exn =
-  (case Option.map #startPosition (PolyML.exceptionLocation exn) of
-    NONE => NONE
-  | SOME i => if i >= 0 then NONE else SOME (~ i));
-
 exception Interrupt = SML90.Interrupt;
 
 use "General/exn.ML";