eliminated fragile catch-all pattern, based on educated guess about the intended exception;
--- 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