1.1 --- a/src/Pure/library.ML	Mon Jul 23 16:45:04 2007 +0200
     1.2 +++ b/src/Pure/library.ML	Mon Jul 23 19:45:44 2007 +0200
     1.3 @@ -34,8 +34,6 @@
     1.4  
     1.5    (*exceptions*)
     1.6    exception EXCEPTION of exn * string
     1.7 -  val do_transform_failure: bool ref
     1.8 -  val transform_failure: (exn -> exn) -> ('a -> 'b) -> 'a -> 'b
     1.9    datatype 'a result = Result of 'a | Exn of exn
    1.10    val capture: ('a -> 'b) -> 'a -> 'b result
    1.11    val release: 'a result -> 'a
    1.12 @@ -273,13 +271,6 @@
    1.13  
    1.14  (* exceptions *)
    1.15  
    1.16 -val do_transform_failure = ref true;
    1.17 -
    1.18 -fun transform_failure exn f x =
    1.19 -  if ! do_transform_failure then
    1.20 -    f x handle Interrupt => raise Interrupt | e => raise exn e
    1.21 -  else f x;
    1.22 -
    1.23  exception EXCEPTION of exn * string;
    1.24  
    1.25  datatype 'a result =