# HG changeset patch
# User blanchet
# Date 1282599131 -7200
# Node ID 185bf5b191a927f64851a4c32131b564fd02528a
# Parent  b2ae937a134bdb7e6cbb038cc3a12659f121a25d
cosmetics

diff -r b2ae937a134b -r 185bf5b191a9 src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Mon Aug 23 23:24:24 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Mon Aug 23 23:32:11 2010 +0200
@@ -345,9 +345,8 @@
             | relevant (new_pairs, rejects) [] =
               let
                 val (new_rels, more_rejects) = take_best max_new new_pairs
-                val new_consts = new_rels |> maps snd
                 val rel_const_tab' =
-                  rel_const_tab |> fold add_const_to_table new_consts
+                  rel_const_tab |> fold add_const_to_table (maps snd new_rels)
                 fun is_dirty c =
                   const_mem rel_const_tab' c andalso
                   not (const_mem rel_const_tab c)