--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Fri May 13 10:10:43 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Fri May 13 10:10:43 2011 +0200
@@ -1095,7 +1095,7 @@
| _ => I)
val (problem, pool) =
problem |> nice_atp_problem (Config.get ctxt readable_names)
- fun add_sym_arity (s, {min_ary, ...}) =
+ fun add_sym_arity (s, {min_ary, ...} : sym_info) =
if min_ary > 0 then
case strip_prefix_and_unascii const_prefix s of
SOME s => Symtab.insert (op =) (s, min_ary)