author | wenzelm |
Tue, 28 Dec 2010 18:28:52 +0100 | |
changeset 41406 | 062490d081b9 |
parent 41405 | 05bd42fdaea8 |
child 41407 | 2878845bc549 |
src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML | file | annotate | diff | comparison | revisions |
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Mon Dec 27 12:33:21 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Tue Dec 28 18:28:52 2010 +0100 @@ -262,7 +262,7 @@ (if is_atp_variable s then I else Symtab.map_entry s (Integer.add 1)) #> fold count_term tms -val count_formula = fold_formula count_term +fun count_formula x = fold_formula count_term x val init_counters = metis_helpers |> map fst |> sort_distinct string_ord |> map (rpair 0)