# HG changeset patch
# User wenzelm
# Date 1288725357 -3600
# Node ID 2bdb14323fbfda0b152ed118773a044c11a37175
# Parent  c753e3f8b4d6d5a3551a81b054c301cc5302b9dc
eliminated fragile catch-all pattern, based on educated guess about the intended exception;

diff -r c753e3f8b4d6 -r 2bdb14323fbf src/HOL/Matrix/matrixlp.ML
--- a/src/HOL/Matrix/matrixlp.ML	Tue Nov 02 12:37:12 2010 +0100
+++ b/src/HOL/Matrix/matrixlp.ML	Tue Nov 02 20:15:57 2010 +0100
@@ -82,7 +82,7 @@
     let
         val simp_th = matrix_compute (cprop_of th)
         val th = Thm.strip_shyps (Thm.equal_elim simp_th th)
-        fun removeTrue th = removeTrue (Thm.implies_elim th TrueI) handle _ => th  (* FIXME avoid handle _ *)
+        fun removeTrue th = removeTrue (Thm.implies_elim th TrueI) handle THM _ => th
     in
         removeTrue th
     end