src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
changeset 41384 c4488b7cbe3b
parent 41313 a96ac4d180b7
child 41406 062490d081b9
--- 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 =