diff -r 6f0f2b71fd69 -r 9552b6f2c670 src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Mon Feb 06 23:01:02 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Mon Feb 06 23:01:02 2012 +0100
@@ -2408,9 +2408,10 @@
           mangle_type_args_in_const format type_enc base_name T_args
         val base_ary = min_ary_of sym_tab0 base_s
         fun do_const name = IConst (name, T, T_args)
-        val do_term =
+        val filter_ty_args =
           filter_type_args_in_iterm thy monom_constrs type_enc
-          #> ho_term_from_iterm ctxt format mono type_enc (SOME true)
+        val ho_term_of =
+          ho_term_from_iterm ctxt format mono type_enc (SOME true)
         val name1 as (s1, _) =
           base_name |> ary - 1 > base_ary ? aliased_uncurried (ary - 1)
         val name2 as (s2, _) = base_name |> aliased_uncurried ary
@@ -2423,12 +2424,15 @@
         val tm1 =
           mk_app_op format type_enc (list_app (do_const name1) first_bounds)
                     last_bound
-        val tm2 = list_app (do_const name2) (first_bounds @ [last_bound])
+          |> filter_ty_args
+        val tm2 =
+          list_app (do_const name2) (first_bounds @ [last_bound])
+          |> filter_ty_args
         val do_bound_type = do_bound_type ctxt format mono type_enc
         val eq =
           eq_formula type_enc (atomic_types_of T)
                      (map (apsnd do_bound_type) bounds) false
-                     (do_term tm1) (do_term tm2)
+                     (ho_term_of tm1) (ho_term_of tm2)
       in
         ([tm1, tm2],
          [Formula (uncurried_alias_eq_prefix ^ s2, kind, eq |> maybe_negate,