src/HOL/Tools/Sledgehammer/metis_tactics.ML
changeset 36230 43d10a494c91
parent 36170 0cdb76723c88
child 36383 6adf1068ac0f
     1.1 --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Mon Apr 19 17:18:21 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Mon Apr 19 18:14:45 2010 +0200
     1.3 @@ -693,13 +693,19 @@
     1.4                  val unused = th_cls_pairs |> map_filter (fn (name, cls) =>
     1.5                    if common_thm used cls then NONE else SOME name)
     1.6              in
     1.7 -                if null unused then ()
     1.8 -                else warning ("Metis: unused theorems " ^ commas_quote unused);
     1.9 +                if not (common_thm used cls) then
    1.10 +                  warning "Metis: The goal is provable because the context is \
    1.11 +                          \inconsistent."
    1.12 +                else if not (null unused) then
    1.13 +                  warning ("Metis: Unused theorems: " ^ commas_quote unused
    1.14 +                           ^ ".")
    1.15 +                else
    1.16 +                  ();
    1.17                  case result of
    1.18                      (_,ith)::_ =>
    1.19 -                        (trace_msg (fn () => "success: " ^ Display.string_of_thm ctxt ith);
    1.20 +                        (trace_msg (fn () => "Success: " ^ Display.string_of_thm ctxt ith);
    1.21                           [ith])
    1.22 -                  | _ => (trace_msg (fn () => "Metis: no result");
    1.23 +                  | _ => (trace_msg (fn () => "Metis: No result");
    1.24                            [])
    1.25              end
    1.26          | Metis.Resolution.Satisfiable _ =>