Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
merged
authorwenzelm
Wed, 22 Dec 2010 14:44:03 +0100
changeset 41385 6476ab765777
parent 41384 c4488b7cbe3b (diff)
parent 41383 514bb82514df (current diff)
child 41386 9400026a82f5
child 41387 fb81cb128e7e
merged
--- 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 =
isabelle