Added an exception handler and error msg.

--- a/src/Provers/Arith/fast_lin_arith.ML	Tue Jan 20 13:56:27 2004 +0100
+++ b/src/Provers/Arith/fast_lin_arith.ML	Sun Jan 25 00:42:22 2004 +0100
@@ -415,7 +415,11 @@
       fun addthms thm1 thm2 =
         case add2 thm1 thm2 of
           None => (case try_add ([thm1] RL inj_thms) thm2 of
-                     None => the(try_add ([thm2] RL inj_thms) thm1)
+                     None => ( the(try_add ([thm2] RL inj_thms) thm1)
+                               handle OPTION =>
+                               (trace_thm "" thm1; trace_thm "" thm2;
+                                sys_error "Lin.arith. failed to add thms")
+                             )
                    | Some thm => thm)
         | Some thm => thm;