1.1 --- a/test/Tools/isac/Knowledge/rational.sml	Thu Apr 29 14:13:11 2021 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/rational.sml	Thu Apr 29 17:02:10 2021 +0200
     1.3 @@ -220,7 +220,7 @@
     1.4                  Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty)
     1.5               in
     1.6                snd (eval__true thy (i + 1) (map (Envir.subst_term subst) pres) [] erls)
     1.7 -             end) handle _ => false
     1.8 +             end) handle Pattern.MATCH => false
     1.9             fun scan_ f [] = false (*scan_ NEVER called by []*)
    1.10               | scan_ f (pp::pps) =
    1.11                 if f pp then true else scan_ f pps;
    1.12 @@ -242,7 +242,7 @@
    1.13                  Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty)
    1.14               in
    1.15                snd (eval__true thy (i + 1) (map (Envir.subst_term subst) pres) [] erls)
    1.16 -             end) handle _ => false
    1.17 +             end) handle Pattern.MATCH => false
    1.18             fun scan_ f [] = false (*scan_ NEVER called by []*)
    1.19               | scan_ f (pp::pps) =
    1.20                 if f pp then true else scan_ f pps;
    1.21 @@ -391,7 +391,7 @@
    1.22                  Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty)
    1.23               in
    1.24                snd (eval__true thy (i + 1) (map (Envir.subst_term subst) pres) [] erls)
    1.25 -             end) handle _ => false
    1.26 +             end) handle Pattern.MATCH => false
    1.27             fun scan_ f [] = false (*scan_ NEVER called by []*)
    1.28               | scan_ f (pp::pps) =
    1.29                 if f pp then true else scan_ f pps;