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