# HG changeset patch
# User blanchet
# Date 1272632301 -7200
# Node ID 6e8a1c5eb0a8c8c323b9eba1b682a4d28c552d44
# Parent  870dfa6d00ce97c078b62debc02895395c6fc648
catch the right exception

diff -r 870dfa6d00ce -r 6e8a1c5eb0a8 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Fri Apr 30 14:52:49 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Fri Apr 30 14:58:21 2010 +0200
@@ -1393,7 +1393,7 @@
                    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