src/Pure/ML/exn_properties.ML

 Exception properties.
 *)
 
 signature EXN_PROPERTIES =
 sig
-  val position_of_location: PolyML.location -> Position.T
+  val position_of_polyml_location: ML_Compiler0.polyml_location -> Position.T
   val position: exn -> Position.T
   val get: exn -> Properties.T
   val update: Properties.entry list -> exn -> exn
 end;
 
 structure Exn_Properties: EXN_PROPERTIES =
 struct
 
 (* source locations *)
 
-fun props_of_location (loc: PolyML.location) =
+fun props_of_polyml_location (loc: ML_Compiler0.polyml_location) =
   (case YXML.parse_body (#file loc) of
     [] => []
   | [XML.Text file] =>
       if file = "Standard Basis" then []
       else [(Markup.fileN, ML_System.standard_path file)]
   | body => XML.Decode.properties body);
 
-fun position_of_location loc =
+fun position_of_polyml_location loc =
   Position.make
    {line = FixedInt.toInt (#startLine loc),
     offset = FixedInt.toInt (#startPosition loc),
     end_offset = FixedInt.toInt (#endPosition loc),
-    props = props_of_location loc};
+    props = props_of_polyml_location loc};
 
 fun position exn =
-  (case PolyML.exceptionLocation exn of
+  (case Exn.polyml_location exn of
     NONE => Position.none
-  | SOME loc => position_of_location loc);
+  | SOME loc => position_of_polyml_location loc);
 
 
 (* exception properties *)
 
 fun get exn =
-  (case PolyML.exceptionLocation exn of
+  (case Exn.polyml_location exn of
     NONE => []
-  | SOME loc => props_of_location loc);
+  | SOME loc => props_of_polyml_location loc);
 
 fun update entries exn =
   if Exn.is_interrupt exn then exn
   else
     let
       val loc =
         the_default {file = "", startLine = 0, endLine = 0, startPosition = 0, endPosition = 0}
-          (PolyML.exceptionLocation exn);
-      val props = props_of_location loc;
+          (Exn.polyml_location exn);
+      val props = props_of_polyml_location loc;
       val props' = fold Properties.put entries props;
     in
       if props = props' then exn
       else
         let