| changeset 39232 | 69c6d3e87660 |
| parent 31480 | 05937d6aafb5 |
| child 41493 | f05976d69141 |
--- a/src/Pure/General/basics.ML Thu Sep 09 11:05:52 2010 +0200 +++ b/src/Pure/General/basics.ML Thu Sep 09 17:20:27 2010 +0200 @@ -94,7 +94,7 @@ (* partiality *) fun try f x = SOME (f x) - handle (exn as Exn.Interrupt) => reraise exn | _ => NONE; + handle exn => if Exn.is_interrupt exn then reraise exn else NONE; fun can f x = is_some (try f x);