# 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