src/Pure/General/basics.ML
changeset 28443 de653f1ad78b
parent 23559 0de527730294
child 29606 fedb8be05f24
     1.1 --- a/src/Pure/General/basics.ML	Wed Oct 01 12:00:01 2008 +0200
     1.2 +++ b/src/Pure/General/basics.ML	Wed Oct 01 12:00:02 2008 +0200
     1.3 @@ -95,7 +95,7 @@
     1.4  (* partiality *)
     1.5  
     1.6  fun try f x = SOME (f x)
     1.7 -  handle Interrupt => raise Interrupt | _ => NONE;
     1.8 +  handle Exn.Interrupt => raise Exn.Interrupt | _ => NONE;
     1.9  
    1.10  fun can f x = is_some (try f x);
    1.11