# HG changeset patch
# User wenzelm
# Date 1470684360 -7200
# Node ID a59d9b81be24457dbad2d9fdd7d792e470acb1e3
# Parent  2edc8da89edcc6c5d4380fd96a871a256dd152a2
Item_Net.retrieve_matching requires beta-eta normal form (amending 8976c5bc9e97);

diff -r 2edc8da89edc -r a59d9b81be24 src/Pure/consts.ML
--- 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 *)