# HG changeset patch
# User blanchet
# Date 1293004963 -3600
# Node ID c4488b7cbe3becf435d181b01cf59874bf358f00
# Parent  a35af5180c0104ff62507e68735a2b5a929f147b
made SML/NJ happy

diff -r a35af5180c01 -r c4488b7cbe3b src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Tue Dec 21 17:52:35 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Wed Dec 22 09:02:43 2010 +0100
@@ -654,9 +654,8 @@
 fun add_term_weights weight (ATerm (s, tms)) =
   (not (is_atp_variable s) andalso s <> "equal") ? Symtab.default (s, weight)
   #> fold (add_term_weights weight) tms
-val add_formula_weights = fold_formula o add_term_weights
 fun add_problem_line_weights weight (Fof (_, _, phi)) =
-  add_formula_weights weight phi
+  fold_formula (add_term_weights weight) phi
 
 fun add_conjectures_weights [] = I
   | add_conjectures_weights conjs =