| changeset 63573 | 8976c5bc9e97 |
| parent 61262 | 7bd1eb4b056e |
| child 63632 | a59d9b81be24 |
--- a/src/Pure/consts.ML Sun Jul 31 22:56:18 2016 +0200 +++ b/src/Pure/consts.ML Mon Aug 01 11:54:32 2016 +0200 @@ -84,7 +84,7 @@ fun retrieve_abbrevs (Consts {rev_abbrevs, ...}) modes = let val nets = map_filter (Symtab.lookup rev_abbrevs) modes - in fn t => maps (fn net => Item_Net.retrieve net t) nets end; + in fn t => maps (fn net => Item_Net.retrieve_matching net t) nets end; (* dest consts *)