--- 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 _ => []))