src/HOL/Tools/Nitpick/nitpick_hol.ML

                    I
                  else
                    cons (T', monomorphic_term (Sign.typ_match thy (T', T)
                                                               Vartab.empty) t)
                    handle Type.TYPE_MATCH => I
-                        | Refute.REFUTE _ =>
+                        | TERM _ =>
                           if slack then
                             I
                           else
                             raise NOT_SUPPORTED ("too much polymorphism in \
                                                  \axiom involving " ^ quote s))