Added an exception handler and error msg.
authornipkow
Sun Jan 25 00:42:22 2004 +0100 (2004-01-25)
changeset 14360e654599b114e
parent 14359 3d9948163018
child 14361 ad2f5da643b4
Added an exception handler and error msg.
src/Provers/Arith/fast_lin_arith.ML
     1.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Tue Jan 20 13:56:27 2004 +0100
     1.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Sun Jan 25 00:42:22 2004 +0100
     1.3 @@ -415,7 +415,11 @@
     1.4        fun addthms thm1 thm2 =
     1.5          case add2 thm1 thm2 of
     1.6            None => (case try_add ([thm1] RL inj_thms) thm2 of
     1.7 -                     None => the(try_add ([thm2] RL inj_thms) thm1)
     1.8 +                     None => ( the(try_add ([thm2] RL inj_thms) thm1)
     1.9 +                               handle OPTION =>
    1.10 +                               (trace_thm "" thm1; trace_thm "" thm2;
    1.11 +                                sys_error "Lin.arith. failed to add thms")
    1.12 +                             )
    1.13                     | Some thm => thm)
    1.14          | Some thm => thm;
    1.15