src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
changeset 42778 896aaab98563
parent 42761 8ea9c6fa8b53
child 42780 be6164bc9744
--- 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)