diff -r 5d9beee36fbe -r e077a0e66563 src/Pure/library.ML
--- a/src/Pure/library.ML	Tue Nov 17 14:05:47 1998 +0100
+++ b/src/Pure/library.ML	Tue Nov 17 14:06:32 1998 +0100
@@ -75,6 +75,7 @@
   val cons: 'a -> 'a list -> 'a list
   val single: 'a -> 'a list
   val append: 'a list -> 'a list -> 'a list
+  val apply: ('a -> 'a) list -> 'a -> 'a
   val foldl: ('a * 'b -> 'a) -> 'a * 'b list -> 'a
   val foldr: ('a * 'b -> 'b) -> 'a list * 'b -> 'b
   val foldr1: ('a * 'a -> 'a) -> 'a list -> 'a
@@ -225,6 +226,7 @@
   val handle_error: ('a -> 'b) -> 'a -> 'b error
   exception ERROR_MESSAGE of string
   val transform_error: ('a -> 'b) -> 'a -> 'b
+  val transform_failure: (exn -> exn) -> ('a -> 'b) -> 'a -> 'b
 
   (*timing*)
   val cond_timeit: bool -> (unit -> 'a) -> 'a
@@ -397,6 +399,9 @@
 
 fun append xs ys = xs @ ys;
 
+fun apply [] x = x
+  | apply (f :: fs) x = apply fs (f x);
+
 
 (* fold *)
 
@@ -1111,6 +1116,12 @@
   | Error msg => raise ERROR_MESSAGE msg);
 
 
+(* transform any exception, including ERROR *)
+
+fun transform_failure exn f x =
+  transform_error f x handle e => raise exn e;
+
+
 
 (** timing **)
 
@@ -1121,7 +1132,7 @@
     let val start = startTiming()
         val result = f ()
     in
-	writeln (endTiming start);  result
+        writeln (endTiming start);  result
     end
   else f ();
 
@@ -1184,7 +1195,7 @@
   | transitive_closure ((x, ys)::ps) =
       let val qs = transitive_closure ps
           val zs = foldl (fn (zs, y) => assocs qs y union_string zs) (ys, ys)
-          fun step(u, us) = (u, if x mem_string us then zs union_string us 
+          fun step(u, us) = (u, if x mem_string us then zs union_string us
                                 else us)
       in (x, zs) :: map step qs end;
 
@@ -1195,15 +1206,15 @@
 local
 (*Maps 0-63 to A-Z, a-z, 0-9 or _ or ' for generating random identifiers*)
 fun char i =      if i<26 then chr (ord "A" + i)
-	     else if i<52 then chr (ord "a" + i - 26)
-	     else if i<62 then chr (ord"0" + i - 52)
-	     else if i=62 then "_"
-	     else  (*i=63*)    "'";
+             else if i<52 then chr (ord "a" + i - 26)
+             else if i<62 then chr (ord"0" + i - 52)
+             else if i=62 then "_"
+             else  (*i=63*)    "'";
 
 val charVec = Vector.tabulate (64, char);
 
-fun newid n = 
-  let 
+fun newid n =
+  let
   in  implode (map (fn i => Vector.sub(charVec,i)) (radixpand (64,n)))  end;
 
 val seedr = ref 0;
@@ -1219,7 +1230,7 @@
 local
 (*Identifies those character codes legal in identifiers.
   chould use Basis Library character functions if Poly/ML provided characters*)
-fun idCode k = (ord "a" <= k andalso k < ord "z") orelse 
+fun idCode k = (ord "a" <= k andalso k < ord "z") orelse
                (ord "A" <= k andalso k < ord "Z") orelse
                (ord "0" <= k andalso k < ord "9");
 
@@ -1233,9 +1244,9 @@
   "_" and "'" are not changed.
   For making variants of identifiers.*)
 
-fun bump_int_list(c::cs) = 
-	if c="9" then "0" :: bump_int_list cs 
-	else
+fun bump_int_list(c::cs) =
+        if c="9" then "0" :: bump_int_list cs
+        else
         if "0" <= c andalso c < "9" then chr(ord(c)+1) :: cs
         else "1" :: c :: cs
   | bump_int_list([]) = error("bump_int_list: not an identifier");
@@ -1245,13 +1256,13 @@
   | bump_list("z"::cs, _) = "a" :: bump_list(cs, "a")
   | bump_list("Z"::cs, _) = "A" :: bump_list(cs, "A")
   | bump_list("9"::cs, _) = "0" :: bump_int_list cs
-  | bump_list(c::cs, _) = 
+  | bump_list(c::cs, _) =
         let val k = ord(c)
-        in if Vector.sub(idCodeVec,k) then chr(k+1) :: cs 
-	   else
-           if c="'" orelse c="_" then c :: bump_list(cs, "") 
-	   else error("bump_list: not legal in identifier: " ^
-		      implode(rev(c::cs)))
+        in if Vector.sub(idCodeVec,k) then chr(k+1) :: cs
+           else
+           if c="'" orelse c="_" then c :: bump_list(cs, "")
+           else error("bump_list: not legal in identifier: " ^
+                      implode(rev(c::cs)))
         end;
 
 end;