| changeset 62505 | 9e2a65912111 |
| parent 61064 | 01b23bfb4947 |
| child 62663 | bea354f6ff21 |
--- 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;