--- a/src/Pure/RAW/exn.ML Mon Jan 18 14:59:59 2016 +0100 +++ b/src/Pure/RAW/exn.ML Mon Jan 18 16:03:18 2016 +0100 @@ -89,4 +89,3 @@ end; datatype illegal = Interrupt; -