# HG changeset patch
# User wenzelm
# Date 1293557332 -3600
# Node ID 062490d081b9d5ef637b3c6daefc12c2dfdbd426
# Parent  05bd42fdaea8780e2995bc36c326c742d0266158
made SML/NJ happy;

diff -r 05bd42fdaea8 -r 062490d081b9 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
--- 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)