# HG changeset patch
# User blanchet
# Date 1304583852 -7200
# Node ID 30278eb9c9db7168175a8ff5d6f0b4c8f2efa622
# Parent  3c2baf9b3c61d7250e79dda7bdb1f9e502779d8d
hopefully this will help the SML/NJ type inference

diff -r 3c2baf9b3c61 -r 30278eb9c9db src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Thu May 05 10:16:14 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Thu May 05 10:24:12 2011 +0200
@@ -887,7 +887,7 @@
       case type_sys of
         Preds (Polymorphic, All_Types) => insert_type #3 decl decls
       | _ => insert (op =) decl decls
-    fun do_term tm =
+    and do_term tm =
       let val (head, args) = strip_combterm_comb tm in
         (case head of
            CombConst ((s, s'), T, T_args) =>