more restrictive retrieval of rules for matching instead of unification -- relevant for performance of printing terms;

--- 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 *)