# HG changeset patch
# User blanchet
# Date 1282721668 -7200
# Node ID 4fe1bb9e74346cbc0cb4098cbb8a18b3d7f6be92
# Parent  7635bf8918a10d28230a3821911a8b040423b927
cosmetics

diff -r 7635bf8918a1 -r 4fe1bb9e7434 src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Wed Aug 25 09:32:43 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Wed Aug 25 09:34:28 2010 +0200
@@ -244,11 +244,9 @@
   in if Real.isFinite res then res else 0.0 end
 *)
 
-(* Multiplies out to a list of pairs: 'a * 'b list -> ('a * 'b) list
-   -> ('a * 'b) list. *)
-fun add_expand_pairs (x, ys) xys = List.foldl (fn (y,acc) => (x,y)::acc) xys ys
 fun consts_of_term thy t =
-  Symtab.fold add_expand_pairs (get_consts thy (SOME true) [t]) []
+  Symtab.fold (fn (x, ys) => fold (fn y => cons (x, y)) ys)
+              (get_consts thy (SOME true) [t]) []
 
 fun pair_consts_axiom theory_relevant thy axiom =
   (axiom, axiom |> snd |> theory_const_prop_of theory_relevant