# HG changeset patch
# User blanchet
# Date 1282908422 -7200
# Node ID 4ec3cbd95f25a8bd265cb5a5477985c47bf6fdb3
# Parent  f74513bbe627aeb2fff90647ac0a956231e7f73a
rename and simplify

diff -r f74513bbe627 -r 4ec3cbd95f25 src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Fri Aug 27 13:19:48 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Fri Aug 27 13:27:02 2010 +0200
@@ -292,7 +292,7 @@
 *)
 
 fun pconsts_in_axiom thy t =
-  Symtab.fold (fn (x, ys) => fold (fn y => cons (x, y)) ys)
+  Symtab.fold (fn (s, pss) => fold (cons o pair s) pss)
               (get_pconsts thy true (SOME true) [t]) []
 fun pair_consts_axiom theory_relevant thy axiom =
   (axiom, axiom |> snd |> theory_const_prop_of theory_relevant