| changeset 31480 | 05937d6aafb5 |
| parent 29606 | fedb8be05f24 |
| child 39232 | 69c6d3e87660 |
--- a/src/Pure/General/basics.ML Sat Jun 06 21:46:36 2009 +0200 +++ b/src/Pure/General/basics.ML Sat Jun 06 21:47:02 2009 +0200 @@ -94,7 +94,7 @@ (* partiality *) fun try f x = SOME (f x) - handle Exn.Interrupt => raise Exn.Interrupt | _ => NONE; + handle (exn as Exn.Interrupt) => reraise exn | _ => NONE; fun can f x = is_some (try f x);