--- 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