# HG changeset patch
# User bulwahn
# Date 1328436865 -3600
# Node ID 0a37c1e52c917b7cd36e07069d525c56bc000233
# Parent  b447318e5e1a6bd55e114b182745cff57564e6fb# Parent  23936fa78841827c057c6a1d62bdab2b23bb2a43
merged

diff -r b447318e5e1a -r 0a37c1e52c91 src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Sun Feb 05 10:43:52 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Sun Feb 05 11:14:25 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