diff -r 0724e56b5dea -r 818ec0118683 src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Tue Dec 20 18:46:05 2011 +0100
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Tue Dec 20 18:59:46 2011 +0100
@@ -739,7 +739,7 @@
 
 (* The Booleans indicate whether all type arguments should be kept. *)
 datatype type_arg_policy =
-  Explicit_Type_Args of bool |
+  Explicit_Type_Args of bool (* infer_from_term_args *) |
   Mangled_Type_Args |
   No_Type_Args
 
@@ -1033,7 +1033,8 @@
                | filter_T_args true = filter_const_type_args thy s'' ary T_args
            in
              case type_arg_policy type_enc s'' of
-               Explicit_Type_Args drop_args => (name, filter_T_args drop_args)
+               Explicit_Type_Args infer_from_term_args =>
+               (name, filter_T_args infer_from_term_args)
              | No_Type_Args => (name, [])
              | Mangled_Type_Args => raise Fail "unexpected (un)mangled symbol"
            end)
@@ -2416,8 +2417,7 @@
          lifted) =
       translate_formulas ctxt format prem_kind type_enc lam_trans preproc hyp_ts
                          concl_t facts
-    val sym_tab =
-      sym_table_for_facts ctxt type_enc explicit_apply conjs facts
+    val sym_tab = sym_table_for_facts ctxt type_enc explicit_apply conjs facts
     val mono = conjs @ facts |> mononotonicity_info_for_facts ctxt type_enc
     val firstorderize = firstorderize_fact thy format type_enc sym_tab
     val (conjs, facts) = (conjs, facts) |> pairself (map firstorderize)
@@ -2426,8 +2426,7 @@
       sym_tab |> helper_facts_for_sym_table ctxt format type_enc
               |> map firstorderize
     val mono_Ts =
-      helpers @ conjs @ facts
-      |> monotonic_types_for_facts ctxt mono type_enc
+      helpers @ conjs @ facts |> monotonic_types_for_facts ctxt mono type_enc
     val class_decl_lines = decl_lines_for_classes type_enc classes
     val sym_decl_lines =
       (conjs, helpers @ facts)