# HG changeset patch
# User wenzelm
# Date 1474403391 -7200
# Node ID 500646ef617a3c067f96948ecc9cb5d2ae14a365
# Parent  f91766530e13db8aa3510cdc6da199284bcaa600
avoid old SML90;

diff -r f91766530e13 -r 500646ef617a src/Pure/General/exn.ML
--- a/src/Pure/General/exn.ML	Sun Sep 18 17:57:55 2016 +0200
+++ b/src/Pure/General/exn.ML	Tue Sep 20 22:29:51 2016 +0200
@@ -85,7 +85,7 @@
 
 (* interrupts *)
 
-exception Interrupt = SML90.Interrupt;
+exception Interrupt = Thread.Thread.Interrupt;
 
 fun interrupt () = raise Interrupt;
 
diff -r f91766530e13 -r 500646ef617a src/Pure/ML/ml_pervasive.ML
--- a/src/Pure/ML/ml_pervasive.ML	Sun Sep 18 17:57:55 2016 +0200
+++ b/src/Pure/ML/ml_pervasive.ML	Tue Sep 20 22:29:51 2016 +0200
@@ -19,7 +19,7 @@
 val ord = SML90.ord;
 val chr = SML90.chr;
 val raw_explode = SML90.explode;
-val implode = SML90.implode;
+val implode = String.concat;
 
 val pointer_eq = PolyML.pointerEq;