src/Pure/ML-Systems/polyml.ML

 
 exception Interrupt = SML90.Interrupt;
 
 use "General/exn.ML";
 
+fun print_exception_trace (_: exn -> string) (_: string -> unit) = PolyML.exception_trace;
+
+if ML_System.name = "polyml-5.5.1"
+  orelse ML_System.name = "polyml-5.5.2"
+  orelse ML_System.name = "polyml-5.5.3"
+then use "ML-Systems/exn_trace_polyml-5.5.1.ML"
+else ();
+
 
 (* multithreading *)
 
 val seconds = Time.fromReal;
 

 fun quit () = exit 0;
 
 
 (* ML runtime system *)
 
-fun print_exception_trace (_: exn -> string) (_: string -> unit) = PolyML.exception_trace;
 val timing = PolyML.timing;
 val profiling = PolyML.profiling;
 
 fun profile 0 f x = f x
   | profile n f x =