src/HOL/Tools/Sledgehammer/metis_tactics.ML
changeset 36383 6adf1068ac0f
parent 36230 43d10a494c91
child 36401 31252c4d4923
     1.1 --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Fri Apr 23 19:36:49 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Sat Apr 24 16:05:42 2010 +0200
     1.3 @@ -693,10 +693,11 @@
     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 not (common_thm used cls) then
     1.8 -                  warning "Metis: The goal is provable because the context is \
     1.9 -                          \inconsistent."
    1.10 -                else if not (null unused) then
    1.11 +                if not (null cls) andalso not (common_thm used cls) then
    1.12 +                  warning "Metis: The assumptions are inconsistent."
    1.13 +                else
    1.14 +                  ();
    1.15 +                if not (null unused) then
    1.16                    warning ("Metis: Unused theorems: " ^ commas_quote unused
    1.17                             ^ ".")
    1.18                  else