# HG changeset patch
# User wenzelm
# Date 1126642765 -7200
# Node ID ca0e5105c4b12a20e10a16b8c9aace6fbf0dee84
# Parent  11f959f0fe6ca81b2a30816ba849d1f5a41504a8
added exception EXCEPTION of exn * string;

diff -r 11f959f0fe6c -r ca0e5105c4b1 src/Pure/library.ML
--- a/src/Pure/library.ML	Tue Sep 13 22:19:24 2005 +0200
+++ b/src/Pure/library.ML	Tue Sep 13 22:19:25 2005 +0200
@@ -54,6 +54,7 @@
   val is_some: 'a option -> bool
   val is_none: 'a option -> bool
 
+  exception EXCEPTION of exn * string
   exception ERROR
   val try: ('a -> 'b) -> 'a -> 'b option
   val can: ('a -> 'b) -> 'a -> bool
@@ -354,10 +355,13 @@
 exception OPTION of invalid;
 
 val the = Option.valOf;
+
 fun these (SOME x) = x
   | these _ = [];
+
 fun the_default x (SOME y) = y
   | the_default x _ = x;
+
 fun the_list (SOME x) = [x]
   | the_list _ = []
 
@@ -372,7 +376,9 @@
   | is_none NONE = true;
 
 
-(* exception handling *)
+(* exceptions *)
+
+exception EXCEPTION of exn * string;
 
 exception ERROR;
 
@@ -1281,7 +1287,8 @@
 
 fun rat_of_int i = rat_of_intinf (IntInf.fromInt i);
 
-val rat0 = rat_of_int 0; 
+val rat0 = rat_of_int 0;
+
 
 (** misc **)