# HG changeset patch
# User wenzelm
# Date 1293025443 -3600
# Node ID 6476ab765777f63abf88557c36d8620b4dad477c
# Parent  c4488b7cbe3becf435d181b01cf59874bf358f00# Parent  514bb82514dffb4d662f36cf8a0f90b5d9ee7bb5
merged

diff -r 514bb82514df -r 6476ab765777 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Wed Dec 22 13:49:06 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Wed Dec 22 14:44:03 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 =