handle Type.TYPE_MATCH, not arbitrary exceptions;

--- a/src/Pure/Tools/find_consts.ML	Wed Sep 30 22:27:20 2009 +0200
+++ b/src/Pure/Tools/find_consts.ML	Wed Sep 30 22:31:16 2009 +0200
@@ -107,7 +107,7 @@
                 val tye = Sign.typ_match thy (qty, ty) Vartab.empty;
                 val sub_size =
                   Vartab.fold (fn (_, (_, t)) => fn n => Term.size_of_typ t + n) tye 0;
-              in SOME sub_size end handle MATCH => NONE
+              in SOME sub_size end handle Type.TYPE_MATCH => NONE
           end
       | make_match (Loose arg) =
           check_const (matches_subtype thy (make_pattern arg) o snd)