# HG changeset patch
# User blanchet
# Date 1328435434 -3600
# Node ID 23936fa78841827c057c6a1d62bdab2b23bb2a43
# Parent  5ab496224729fe1d0278f959e18e22ea1b16737c
removed double filtering of type args

diff -r 5ab496224729 -r 23936fa78841 src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Sun Feb 05 08:57:03 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Sun Feb 05 10:50:34 2012 +0100
@@ -2407,9 +2407,6 @@
         val (base_name as (base_s, _), T_args) =
           mangle_type_args_in_const format type_enc base_name T_args
         val base_ary = min_ary_of sym_tab0 base_s
-        val T_args =
-          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 =
           filter_type_args_in_iterm thy monom_constrs type_enc