# HG changeset patch
# User wenzelm
# Date 1254342676 -7200
# Node ID a7b92f98180b0ad08814e81eafd40ed605342372
# Parent  d89327de0b3ce92b6cb873a0b6e8d8571d1a968f
handle Type.TYPE_MATCH, not arbitrary exceptions;

diff -r d89327de0b3c -r a7b92f98180b src/Pure/Tools/find_consts.ML
--- 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)