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