# HG changeset patch
# User haftmann
# Date 1125213502 -7200
# Node ID d871853e13e03755b0f1a5faa0298a1905a1c219
# Parent  a696a3d30b97ba859c743b417a95b0e4ddd922f2
added 'these', removed assoc2

diff -r a696a3d30b97 -r d871853e13e0 src/Pure/library.ML
--- a/src/Pure/library.ML	Sun Aug 28 09:02:42 2005 +0200
+++ b/src/Pure/library.ML	Sun Aug 28 09:18:22 2005 +0200
@@ -48,6 +48,7 @@
 
   (*options*)
   val the: 'a option -> 'a
+  val these: 'a list option -> 'a list
   val if_none: 'a option -> 'a -> 'a
   val is_some: 'a option -> bool
   val is_none: 'a option -> bool
@@ -220,13 +221,12 @@
   val duplicates: ''a list -> ''a list
   val has_duplicates: ('a * 'a -> bool) -> 'a list -> bool
 
-  (*association lists*)
+  (*association lists -- see also Pure/General/alist.ML*)
   val assoc: (''a * 'b) list * ''a -> 'b option
   val assoc_int: (int * 'a) list * int -> 'a option
   val assoc_string: (string * 'a) list * string -> 'a option
   val assoc_string_int: ((string * int) * 'a) list * (string * int) -> 'a option
   val assocs: (''a * 'b list) list -> ''a -> 'b list
-  val assoc2: (''a * (''b * 'c) list) list * (''a * ''b) -> 'c option
   val gen_assoc: ('a * 'b -> bool) -> ('b * 'c) list * 'a -> 'c option
   val overwrite: (''a * 'b) list * (''a * 'b) -> (''a * 'b) list
   val gen_overwrite: ('a * 'a -> bool) -> ('a * 'b) list * ('a * 'b) -> ('a * 'b) list
@@ -353,6 +353,8 @@
 exception OPTION of invalid;
 
 val the = Option.valOf;
+fun these (SOME x) = x
+  | these _ = []
 
 (*strict!*)
 fun if_none NONE y = y
@@ -1045,16 +1047,7 @@
   | assoc_string_int ((keyi, xi) :: pairs, key) =
       if key = keyi then SOME xi else assoc_string_int (pairs, key);
 
-fun assocs ps x =
-  (case assoc (ps, x) of
-    NONE => []
-  | SOME ys => ys);
-
-(*two-fold association list lookup*)
-fun assoc2 (aal, (key1, key2)) =
-  (case assoc (aal, key1) of
-    SOME al => assoc (al, key2)
-  | NONE => NONE);
+fun assocs z = curry (these o assoc) z
 
 (*generalized association list lookup*)
 fun gen_assoc eq ([], key) = NONE