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