# HG changeset patch
# User nipkow
# Date 1074987742 -3600
# Node ID e654599b114ec2dab0b37000265cda39240a5948
# Parent  3d99481630181d07a69c2bc33f7ae5f35099641f
Added an exception handler and error msg.

diff -r 3d9948163018 -r e654599b114e src/Provers/Arith/fast_lin_arith.ML
--- 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;