Item_Net.retrieve_matching requires beta-eta normal form (amending 8976c5bc9e97);

--- a/src/Pure/consts.ML	Mon Aug 08 19:39:23 2016 +0200
+++ b/src/Pure/consts.ML	Mon Aug 08 21:26:00 2016 +0200
@@ -83,8 +83,15 @@
   Symtab.map_default (mode, empty_abbrevs) (Item_Net.update abbrs);
 
 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_matching net t) nets end;
+  let val nets = map_filter (Symtab.lookup rev_abbrevs) modes in
+    fn t =>
+      let
+        val retrieve =
+          if Term.could_beta_eta_contract t
+          then Item_Net.retrieve
+          else Item_Net.retrieve_matching
+      in maps (fn net => retrieve net t) nets end
+  end;
 
 
 (* dest consts *)