diff -r c1e3c8508fd2 -r daca5b594fb3 src/Pure/library.ML
--- a/src/Pure/library.ML	Thu May 19 14:06:37 1994 +0200
+++ b/src/Pure/library.ML	Thu May 19 16:12:37 1994 +0200
@@ -17,6 +17,10 @@
 fun I x = x;
 fun K x y = x;
 
+(*reverse apply*)
+infix also;
+fun (x also f) = f x;
+
 (*combine two functions forming the union of their domains*)
 infix orelf;
 fun f orelf g = fn x => f x handle Match => g x;
@@ -118,6 +122,13 @@
   in boolf end;
 
 
+(* flags *)
+
+fun set flag = (flag := true; true);
+fun reset flag = (flag := false; false);
+fun toggle flag = (flag := not (! flag); ! flag);
+
+
 
 (** lists **)
 
@@ -240,8 +251,25 @@
       | Some y => y :: mapfilter f xs);
 
 
+fun find_first _ [] = None
+  | find_first pred (x :: xs) =
+      if pred x then Some x else find_first pred xs;
+
+
 (* lists of pairs *)
 
+fun map2 _ ([], []) = []
+  | map2 f (x :: xs, y :: ys) = (f (x, y) :: map2 f (xs, ys))
+  | map2 _ _ = raise LIST "map2";
+
+fun exists2 _ ([], []) = false
+  | exists2 pred (x :: xs, y :: ys) = pred (x, y) orelse exists2 pred (xs, ys)
+  | exists2 _ _ = raise LIST "exists2";
+
+fun forall2 _ ([], []) = true
+  | forall2 pred (x :: xs, y :: ys) = pred (x, y) andalso forall2 pred (xs, ys)
+  | forall2 _ _ = raise LIST "forall2";
+
 (*combine two lists forming a list of pairs:
   [x1, ..., xn] ~~ [y1, ..., yn]  ===>  [(x1, y1), ..., (xn, yn)]*)
 infix ~~;
@@ -249,10 +277,6 @@
   | (x :: xs) ~~ (y :: ys) = (x, y) :: (xs ~~ ys)
   | _ ~~ _ = raise LIST "~~";
 
-(*combine two lists*)
-fun map2 _ ([], []) = []
-  | map2 f (x :: xs, y :: ys) = (f (x, y) :: map2 f (xs, ys))
-  | map2 _ _ = raise LIST "map2";
 
 (*inverse of ~~; the old 'split':
   [(x1, y1), ..., (xn, yn)]  ===>  ([x1, ..., xn], [y1, ..., yn])*)
@@ -386,6 +410,7 @@
 fun space_implode a bs = implode (separate a bs);
 
 val commas = space_implode ", ";
+val commas_quote = commas o map quote;
 
 (*concatenate messages, one per line, into a string*)
 val cat_lines = space_implode "\n";
@@ -566,6 +591,11 @@
 val extend_list = generic_extend (op =) I I;
 val merge_lists = generic_merge (op =) I I;
 
+fun merge_rev_lists xs [] = xs
+  | merge_rev_lists [] ys = ys
+  | merge_rev_lists xs (y :: ys) =
+      (if y mem xs then I else cons y) (merge_rev_lists xs ys);
+
 
 
 (** balanced trees **)
@@ -612,7 +642,7 @@
 (*print error message and abort to top level*)
 exception ERROR;
 fun error msg = (writeln msg; raise ERROR);
-fun sys_error msg = (writeln "*** System Error ***"; error msg);
+fun sys_error msg = (writeln "*** SYSTEM ERROR ***"; error msg);
 
 fun assert p msg = if p then () else error msg;
 fun deny p msg = if p then error msg else ();