Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
merged
authorbulwahn
Sun, 05 Feb 2012 11:14:25 +0100
changeset 46425 0a37c1e52c91
parent 46424 b447318e5e1a (current diff)
parent 46422 23936fa78841 (diff)
child 46426 fd15abc50fc1
merged
--- 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
isabelle