--- 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