changeset 61770 | a20048c78891 |
parent 61329 | 426c9c858099 |
child 61860 | 2ce3d12015b3 |
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Dec 01 22:21:40 2015 +0100 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Dec 01 22:24:37 2015 +0100 @@ -1715,7 +1715,7 @@ fun specialize_helper t T = if unmangled_s = app_op_name then let val tyenv = Sign.typ_match thy (alpha_to_beta, domain_type T) Vartab.empty in - monomorphic_term tyenv t + Envir.subst_term_types tyenv t end else specialize_type thy (invert_const unmangled_s, T) t