# HG changeset patch
# User smolkas
# Date 1357221948 -3600
# Node ID eb67eec63a8b04850b6065892e91d37e26766cd4
# Parent  df8ae0590be22062e662b6e5f7b34b4dd9a230b2
tuned

diff -r df8ae0590be2 -r eb67eec63a8b src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML	Thu Jan 03 09:56:39 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML	Thu Jan 03 15:05:48 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 _ => []))