# HG changeset patch # User paulson # Date 975060458 -3600 # Node ID b9f7adf3ff11e9eaa002ea025d691d3e0a3b396b # Parent dc113303d10161822ee6e9f8c463ee33f8f9945e added exception Interrupt for use in function Library/try diff -r dc113303d101 -r b9f7adf3ff11 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 =