# HG changeset patch
# User wenzelm
# Date 1326452106 -3600
# Node ID 78175db15b9180bec4723b022f23dca53feea348
# Parent  afdc69f5156edce7230f13cf3a6afaf436cae2b3
handle specific exception, not arbitrary ones (including Interrupt);

diff -r afdc69f5156e -r 78175db15b91 src/HOL/Import/proof_kernel.ML
--- a/src/HOL/Import/proof_kernel.ML	Fri Jan 13 11:50:28 2012 +0100
+++ b/src/HOL/Import/proof_kernel.ML	Fri Jan 13 11:55:06 2012 +0100
@@ -210,7 +210,7 @@
         val tn = no_vars ctxt t'
         fun match u =
             let val _ = Thm.match (ct, cterm_of (Proof_Context.theory_of ctxt) u) in true end
-            handle MATCH => false
+            handle Pattern.MATCH => false
         fun G 0 f ctxt x = f ctxt x
           | G 1 f ctxt x = f (Config.put show_types true ctxt) x
           | G 2 f ctxt x = G 1 f (Config.put show_sorts true ctxt) x