# HG changeset patch
# User wenzelm
# Date 1683375509 -7200
# Node ID ca11a87bd2c6deee1c2070bf7f9dc7e1d4c2d4b8
# Parent  a7ca67369755173c9c6f2cbf8345298fbc229ec6
more operations;

diff -r a7ca67369755 -r ca11a87bd2c6 src/Pure/General/change_table.ML
--- a/src/Pure/General/change_table.ML	Sat May 06 13:42:03 2023 +0200
+++ b/src/Pure/General/change_table.ML	Sat May 06 14:18:29 2023 +0200
@@ -30,6 +30,7 @@
   val map_entry: key -> ('a -> 'a) -> 'a T -> 'a T
   val map_default: key * 'a -> ('a -> 'a) -> 'a T -> 'a T
   val delete_safe: key -> 'a T -> 'a T
+  val lookup_list: 'a list T -> Table.key -> 'a list
   val insert_list: ('a * 'a -> bool) -> key * 'a -> 'a list T -> 'a list T
   val remove_list: ('b * 'a -> bool) -> key * 'b -> 'a list T -> 'a list T
   val update_list: ('a * 'a -> bool) -> key * 'a -> 'a list T -> 'a list T
@@ -160,6 +161,7 @@
 fun map_default (key, x) f = change_table key (Table.map_default (key, x) f);
 fun delete_safe key        = change_table key (Table.delete_safe key);
 
+fun lookup_list arg = Table.lookup_list (table_of arg);
 fun insert_list eq (key, x) = change_table key (Table.insert_list eq (key, x));
 fun remove_list eq (key, x) = change_table key (Table.remove_list eq (key, x));
 fun update_list eq (key, x) = change_table key (Table.update_list eq (key, x));