handle Type.TYPE_MATCH, not arbitrary exceptions;
authorwenzelm
Wed Sep 30 22:31:16 2009 +0200 (2009-09-30)
changeset 32790a7b92f98180b
parent 32789 d89327de0b3c
child 32791 e6d47ce70d27
handle Type.TYPE_MATCH, not arbitrary exceptions;
src/Pure/Tools/find_consts.ML
     1.1 --- a/src/Pure/Tools/find_consts.ML	Wed Sep 30 22:27:20 2009 +0200
     1.2 +++ b/src/Pure/Tools/find_consts.ML	Wed Sep 30 22:31:16 2009 +0200
     1.3 @@ -107,7 +107,7 @@
     1.4                  val tye = Sign.typ_match thy (qty, ty) Vartab.empty;
     1.5                  val sub_size =
     1.6                    Vartab.fold (fn (_, (_, t)) => fn n => Term.size_of_typ t + n) tye 0;
     1.7 -              in SOME sub_size end handle MATCH => NONE
     1.8 +              in SOME sub_size end handle Type.TYPE_MATCH => NONE
     1.9            end
    1.10        | make_match (Loose arg) =
    1.11            check_const (matches_subtype thy (make_pattern arg) o snd)