# HG changeset patch
# User wenzelm
# Date 975071349 -3600
# Node ID 20d4899f5d481707855d2f76274772e66ed99036
# Parent  b9f7adf3ff11e9eaa002ea025d691d3e0a3b396b
exception Interrupt = SML90.Interrupt;

diff -r b9f7adf3ff11 -r 20d4899f5d48 src/Pure/ML-Systems/polyml-4.0.ML
--- a/src/Pure/ML-Systems/polyml-4.0.ML	Fri Nov 24 11:07:38 2000 +0100
+++ b/src/Pure/ML-Systems/polyml-4.0.ML	Fri Nov 24 14:09:09 2000 +0100
@@ -96,7 +96,7 @@
 
 (** interrupts **)
 
-exception Interrupt;
+exception Interrupt = SML90.Interrupt;
 
 local