# HG changeset patch
# User blanchet
# Date 1271698890 -7200
# Node ID 1263bef003b3ff3cc235f725cf4f9041055339b8
# Parent  4d425766a47f27601feb4dda2d15a97f45f02436
cosmetics

diff -r 4d425766a47f -r 1263bef003b3 src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Mon Apr 19 19:41:15 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Mon Apr 19 19:41:30 2010 +0200
@@ -436,15 +436,16 @@
 fun count_constants_term toplev t (const_min_arity, const_needs_hBOOL) =
   let val (head, args) = strip_combterm_comb t
       val n = length args
-      val (const_min_arity, const_needs_hBOOL) = fold (count_constants_term false) args (const_min_arity, const_needs_hBOOL)
+      val (const_min_arity, const_needs_hBOOL) =
+        (const_min_arity, const_needs_hBOOL)
+        |> fold (count_constants_term false) args
   in
       case head of
           CombConst ((a, _),_,_) => (*predicate or function version of "equal"?*)
             let val a = if a="equal" andalso not toplev then "c_fequal" else a
-            val const_min_arity = Symtab.map_default (a, n) (Integer.min n) const_min_arity
             in
-              if toplev then (const_min_arity, const_needs_hBOOL)
-              else (const_min_arity, Symtab.update (a,true) (const_needs_hBOOL))
+              (const_min_arity |> Symtab.map_default (a, n) (Integer.min n),
+               const_needs_hBOOL |> not toplev ? Symtab.update (a, true))
             end
         | _ => (const_min_arity, const_needs_hBOOL)
   end;