tuned error messages
authorhaftmann
Mon Mar 23 19:01:16 2009 +0100 (2009-03-23 ago)
changeset 3068716f6efd4e599
parent 30686 47a32dd1b86e
child 30688 2d1d426e00e4
tuned error messages
src/Provers/Arith/fast_lin_arith.ML
     1.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Mon Mar 23 19:01:16 2009 +0100
     1.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Mon Mar 23 19:01:16 2009 +0100
     1.3 @@ -466,7 +466,7 @@
     1.4                       NONE => ( the (try_add ([thm2] RL inj_thms) thm1)
     1.5                                 handle Option =>
     1.6                                 (trace_thm "" thm1; trace_thm "" thm2;
     1.7 -                                sys_error "Lin.arith. failed to add thms")
     1.8 +                                sys_error "Linear arithmetic: failed to add thms")
     1.9                               )
    1.10                     | SOME thm => thm)
    1.11          | SOME thm => thm;
    1.12 @@ -588,8 +588,8 @@
    1.13            handle NoEx => NONE
    1.14        in
    1.15          case ex of
    1.16 -          SOME s => (warning "arith failed - see trace for a counterexample"; tracing s)
    1.17 -        | NONE => warning "arith failed"
    1.18 +          SOME s => (warning "Linear arithmetic failed - see trace for a counterexample."; tracing s)
    1.19 +        | NONE => warning "Linear arithmetic failed"
    1.20        end;
    1.21  
    1.22  (* ------------------------------------------------------------------------- *)