# HG changeset patch
# User haftmann
# Date 1237831276 -3600
# Node ID 16f6efd4e599a529107d4301bb6c5bd862526b2a
# Parent  47a32dd1b86e397edd27862250bd92e398b18d0b
tuned error messages

diff -r 47a32dd1b86e -r 16f6efd4e599 src/Provers/Arith/fast_lin_arith.ML
--- a/src/Provers/Arith/fast_lin_arith.ML	Mon Mar 23 19:01:16 2009 +0100
+++ b/src/Provers/Arith/fast_lin_arith.ML	Mon Mar 23 19:01:16 2009 +0100
@@ -466,7 +466,7 @@
                      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")
+                                sys_error "Linear arithmetic: failed to add thms")
                              )
                    | SOME thm => thm)
         | SOME thm => thm;
@@ -588,8 +588,8 @@
           handle NoEx => NONE
       in
         case ex of
-          SOME s => (warning "arith failed - see trace for a counterexample"; tracing s)
-        | NONE => warning "arith failed"
+          SOME s => (warning "Linear arithmetic failed - see trace for a counterexample."; tracing s)
+        | NONE => warning "Linear arithmetic failed"
       end;
 
 (* ------------------------------------------------------------------------- *)