added exception Interrupt for use in function Library/try
authorpaulson
Fri, 24 Nov 2000 11:07:38 +0100
changeset 10517 b9f7adf3ff11
parent 10516 dc113303d101
child 10518 20d4899f5d48
added exception Interrupt for use in function Library/try
src/Pure/ML-Systems/polyml-4.0.ML
--- a/src/Pure/ML-Systems/polyml-4.0.ML	Thu Nov 23 21:33:14 2000 +0100
+++ b/src/Pure/ML-Systems/polyml-4.0.ML	Fri Nov 24 11:07:38 2000 +0100
@@ -96,6 +96,8 @@
 
 (** interrupts **)
 
+exception Interrupt;
+
 local
 
 datatype 'a result =