avoid old SML90;
authorwenzelm
Tue, 20 Sep 2016 22:29:51 +0200
changeset 63925 500646ef617a
parent 63924 f91766530e13
child 63926 70973a1b4ec0
avoid old SML90;
src/Pure/General/exn.ML
src/Pure/ML/ml_pervasive.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;
 
--- 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;