# HG changeset patch
# User smolkas
# Date 1357259972 -3600
# Node ID 3e6eb9c4fc6d3285fa1394daf05d85a79137d94a
# Parent  eb67eec63a8b04850b6065892e91d37e26766cd4# Parent  32007a8db6bbe942ec709081dcefe16af1c6419c
merged

diff -r 32007a8db6bb -r 3e6eb9c4fc6d src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML	Thu Jan 03 23:00:32 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML	Fri Jan 04 01:39:32 2013 +0100
@@ -89,13 +89,13 @@
         | update_table (i, Prove (_, l, _, _)) = Label_Table.update_new (l, i)
         | update_table _ = I
       val label_index_table = fold_index update_table proof Label_Table.empty
-      val filter_refs = map_filter (Label_Table.lookup label_index_table)
+      val lookup_indices = map_filter (Label_Table.lookup label_index_table)
 
       (* proof references *)
-      fun refs (Obtain (_, _, _, _, By_Metis (lfs, _))) = filter_refs lfs
-        | refs (Prove (_, _, _, By_Metis (lfs, _))) = filter_refs lfs
+      fun refs (Obtain (_, _, _, _, By_Metis (lfs, _))) = lookup_indices lfs
+        | refs (Prove (_, _, _, By_Metis (lfs, _))) = lookup_indices lfs
         | refs (Prove (_, _, _, Case_Split (cases, (lfs, _)))) =
-          filter_refs lfs @ maps (maps refs) cases
+          lookup_indices lfs @ maps (maps refs) cases
         | refs _ = []
       val refed_by_vect =
         Vector.tabulate (n, (fn _ => []))