# HG changeset patch
# User wenzelm
# Date 1456691155 -3600
# Node ID 4b2018eb92e83648142eb82cb0bac12d1eb34fe9
# Parent  7a5d88dd8cc9ceeee40509fe72bc4bc97f2f941e
clarified;

diff -r 7a5d88dd8cc9 -r 4b2018eb92e8 src/Pure/RAW/ROOT_polyml.ML
--- a/src/Pure/RAW/ROOT_polyml.ML	Sun Feb 28 21:20:51 2016 +0100
+++ b/src/Pure/RAW/ROOT_polyml.ML	Sun Feb 28 21:25:55 2016 +0100
@@ -61,7 +61,7 @@
 
 if ML_System.name = "polyml-5.6"
 then use "RAW/exn_trace.ML"
-else use "RAW/exn_trace_dummy.ML";
+else use "RAW/exn_trace_raw.ML";
 
 
 (* multithreading *)
diff -r 7a5d88dd8cc9 -r 4b2018eb92e8 src/Pure/RAW/exn_trace_dummy.ML
--- a/src/Pure/RAW/exn_trace_dummy.ML	Sun Feb 28 21:20:51 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,7 +0,0 @@
-(*  Title:      Pure/RAW/exn_trace.ML
-    Author:     Makarius
-
-Exception trace dummy.
-*)
-
-fun print_exception_trace (_: exn -> string) (_: string -> unit) = PolyML.exception_trace;
diff -r 7a5d88dd8cc9 -r 4b2018eb92e8 src/Pure/RAW/exn_trace_raw.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/RAW/exn_trace_raw.ML	Sun Feb 28 21:25:55 2016 +0100
@@ -0,0 +1,8 @@
+(*  Title:      Pure/RAW/exn_trace_raw.ML
+    Author:     Makarius
+
+Raw exception trace for Poly/ML 5.3.0.
+*)
+
+fun print_exception_trace (_: exn -> string) (_: string -> unit) =
+  PolyML.exception_trace;
diff -r 7a5d88dd8cc9 -r 4b2018eb92e8 src/Pure/ROOT
--- a/src/Pure/ROOT	Sun Feb 28 21:20:51 2016 +0100
+++ b/src/Pure/ROOT	Sun Feb 28 21:25:55 2016 +0100
@@ -8,7 +8,7 @@
     "RAW/compiler_polyml.ML"
     "RAW/exn.ML"
     "RAW/exn_trace.ML"
-    "RAW/exn_trace_dummy.ML"
+    "RAW/exn_trace_raw.ML"
     "RAW/fixed_int_dummy.ML"
     "RAW/ml_compiler_parameters.ML"
     "RAW/ml_compiler_parameters_polyml-5.6.ML"
@@ -40,7 +40,7 @@
     "RAW/compiler_polyml.ML"
     "RAW/exn.ML"
     "RAW/exn_trace.ML"
-    "RAW/exn_trace_dummy.ML"
+    "RAW/exn_trace_raw.ML"
     "RAW/fixed_int_dummy.ML"
     "RAW/ml_compiler_parameters.ML"
     "RAW/ml_compiler_parameters_polyml-5.6.ML"