handle specific exception, not arbitrary ones (including Interrupt);

--- 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