src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML

       val thy = Proof_Context.theory_of ctxt
       val unmangled_s = mangled_s |> unmangled_const_name
       fun dub_and_inst c needs_full_types (th, j) =
         ((c ^ "_" ^ string_of_int j ^ (if needs_full_types then "ft" else ""),
           false),
-         th |> prop_of
-            |> general_type_arg_policy type_sys = Mangled_Types
-               ? (case typ of
-                    SOME T =>
-                    specialize_type thy (safe_invert_const unmangled_s, T)
-                  | NONE => I))
+         let val t = th |> prop_of in
+           t |> (general_type_arg_policy type_sys = Mangled_Types andalso
+                 not (null (Term.hidden_polymorphism t)))
+                ? (case typ of
+                     SOME T =>
+                     specialize_type thy (safe_invert_const unmangled_s, T)
+                   | NONE => I)
+         end)
       fun make_facts eq_as_iff =
         map_filter (make_fact ctxt false eq_as_iff false)
     in
       metis_helpers
       |> maps (fn (metis_s, (needs_full_types, ths)) =>