# HG changeset patch
# User blanchet
# Date 1328353698 -3600
# Node ID 78ff6a886b50a75a8913942f67efe5c9c20385bd
# Parent  d4754183ccce7a6794fff3e679f8f6a37c8ca7c8
made sure to filter type args also for "uncurried alias" equations

diff -r d4754183ccce -r 78ff6a886b50 src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Sat Feb 04 12:08:18 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Sat Feb 04 12:08:18 2012 +0100
@@ -1523,7 +1523,7 @@
 fun list_app head args = fold (curry (IApp o swap)) args head
 fun predicator tm = IApp (predicator_combconst, tm)
 
-fun do_app_op format type_enc head arg =
+fun mk_app_op format type_enc head arg =
   let
     val head_T = ityp_of head
     val (arg_T, res_T) = dest_funT head_T
@@ -1535,7 +1535,7 @@
 fun firstorderize_fact thy monom_constrs format type_enc sym_tab
                        uncurried_aliases =
   let
-    fun do_app arg head = do_app_op format type_enc head arg
+    fun do_app arg head = mk_app_op format type_enc head arg
     fun list_app_ops head args = fold do_app args head
     fun introduce_app_ops tm =
       let val (head, args) = tm |> strip_iterm_comb ||> map introduce_app_ops in
@@ -2411,7 +2411,9 @@
           T_args |> filter_type_args_in_const thy monom_constrs type_enc
                                               base_ary base_s
         fun do_const name = IConst (name, T, T_args)
-        val do_term = ho_term_from_iterm ctxt format mono type_enc (SOME true)
+        val do_term =
+          filter_type_args_in_iterm thy monom_constrs type_enc
+          #> 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
@@ -2422,7 +2424,7 @@
         val (first_bounds, last_bound) =
           bounds |> map (fn (name, T) => IConst (name, T, [])) |> split_last
         val tm1 =
-          do_app_op format type_enc (list_app (do_const name1) first_bounds)
+          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])
         val do_bound_type = do_bound_type ctxt format mono type_enc