# HG changeset patch
# User wenzelm
# Date 1453129398 -3600
# Node ID 7217adc19be9533a71e93a747c5bf4015b33de85
# Parent  f354900ac0ea233218811a4cdce10e452f8bd2fb
tuned whitespace;

diff -r f354900ac0ea -r 7217adc19be9 src/Pure/RAW/exn.ML
--- 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;
-