src/Pure/library.ML

--- a/src/Pure/library.ML	Wed May 13 12:23:28 1998 +0200
+++ b/src/Pure/library.ML	Wed May 13 19:05:50 1998 +0200
@@ -215,6 +215,8 @@
   val get_error: 'a error -> string option
   val get_ok: 'a error -> 'a option
   val handle_error: ('a -> 'b) -> 'a -> 'b error
+  exception ERROR_MESSAGE of string
+  val transform_error: ('a -> 'b) -> 'a -> 'b
 
   (*timing*)
   val cond_timeit: bool -> (unit -> 'a) -> 'a
@@ -1061,6 +1063,16 @@
   end;
 
 
+(* transform ERROR into ERROR_MESSAGE, capturing the side-effect *)
+
+exception ERROR_MESSAGE of string;
+
+fun transform_error f x =
+  (case handle_error f x of
+    OK y => y
+  | Error msg => raise ERROR_MESSAGE msg);
+
+
 
 (** timing **)