# HG changeset patch
# User blanchet
# Date 1305274243 -7200
# Node ID 896aaab98563baa61851ac1fd9d0cbc600b5c5a5
# Parent  69640564a3941ff667c0c6fe0d7c52c943da0802
make SML/NJ happy

diff -r 69640564a394 -r 896aaab98563 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
--- 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)