--- 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;
--- 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;