1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Wed Aug 25 09:32:43 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Wed Aug 25 09:34:28 2010 +0200
     1.3 @@ -244,11 +244,9 @@
     1.4    in if Real.isFinite res then res else 0.0 end
     1.5  *)
     1.6  
     1.7 -(* Multiplies out to a list of pairs: 'a * 'b list -> ('a * 'b) list
     1.8 -   -> ('a * 'b) list. *)
     1.9 -fun add_expand_pairs (x, ys) xys = List.foldl (fn (y,acc) => (x,y)::acc) xys ys
    1.10  fun consts_of_term thy t =
    1.11 -  Symtab.fold add_expand_pairs (get_consts thy (SOME true) [t]) []
    1.12 +  Symtab.fold (fn (x, ys) => fold (fn y => cons (x, y)) ys)
    1.13 +              (get_consts thy (SOME true) [t]) []
    1.14  
    1.15  fun pair_consts_axiom theory_relevant thy axiom =
    1.16    (axiom, axiom |> snd |> theory_const_prop_of theory_relevant