1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Mon Apr 19 19:41:15 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Mon Apr 19 19:41:30 2010 +0200
     1.3 @@ -436,15 +436,16 @@
     1.4  fun count_constants_term toplev t (const_min_arity, const_needs_hBOOL) =
     1.5    let val (head, args) = strip_combterm_comb t
     1.6        val n = length args
     1.7 -      val (const_min_arity, const_needs_hBOOL) = fold (count_constants_term false) args (const_min_arity, const_needs_hBOOL)
     1.8 +      val (const_min_arity, const_needs_hBOOL) =
     1.9 +        (const_min_arity, const_needs_hBOOL)
    1.10 +        |> fold (count_constants_term false) args
    1.11    in
    1.12        case head of
    1.13            CombConst ((a, _),_,_) => (*predicate or function version of "equal"?*)
    1.14              let val a = if a="equal" andalso not toplev then "c_fequal" else a
    1.15 -            val const_min_arity = Symtab.map_default (a, n) (Integer.min n) const_min_arity
    1.16              in
    1.17 -              if toplev then (const_min_arity, const_needs_hBOOL)
    1.18 -              else (const_min_arity, Symtab.update (a,true) (const_needs_hBOOL))
    1.19 +              (const_min_arity |> Symtab.map_default (a, n) (Integer.min n),
    1.20 +               const_needs_hBOOL |> not toplev ? Symtab.update (a, true))
    1.21              end
    1.22          | _ => (const_min_arity, const_needs_hBOOL)
    1.23    end;