diff -r f14f17e656a6 -r 9e2a65912111 src/Pure/morphism.ML
--- a/src/Pure/morphism.ML	Thu Mar 03 14:03:06 2016 +0100
+++ b/src/Pure/morphism.ML	Thu Mar 03 15:23:02 2016 +0100
@@ -52,7 +52,8 @@
 exception MORPHISM of string * exn;
 
 fun app (name, f) x = f x
-  handle exn => if Exn.is_interrupt exn then reraise exn else raise MORPHISM (name, exn);
+  handle exn =>
+    if Exn.is_interrupt exn then Exn.reraise exn else raise MORPHISM (name, exn);
 
 fun apply fs = fold_rev app fs;