diff -r 2cd36f4c5d65 -r a20048c78891 src/HOL/Tools/ATP/atp_problem_generate.ML
--- 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