# HG changeset patch
# User paulson
# Date 1225188344 -3600
# Node ID fb92b1d1b28538cdd4720ce3817c4c8c13cf851f
# Parent  32b6a8f12c1cf37617688dde8e1f390d0f6ccbb6
The metis method no longer fails because the theorem is too trivial

diff -r 32b6a8f12c1c -r fb92b1d1b285 NEWS
--- a/NEWS	Tue Oct 28 11:03:07 2008 +0100
+++ b/NEWS	Tue Oct 28 11:05:44 2008 +0100
@@ -206,6 +206,9 @@
 * The metis method now fails in the usual manner, rather than raising
 an exception, if it determines that it cannot prove the theorem.
 
+* The metis method no longer fails because the theorem is too trivial
+(contains the empty clause).
+
 * Methods "case_tac" and "induct_tac" now refer to the very same rules
 as the structured Isar versions "cases" and "induct", cf. the
 corresponding "cases" and "induct" attributes.  Mutual induction rules
diff -r 32b6a8f12c1c -r fb92b1d1b285 src/HOL/Tools/metis_tools.ML
--- a/src/HOL/Tools/metis_tools.ML	Tue Oct 28 11:03:07 2008 +0100
+++ b/src/HOL/Tools/metis_tools.ML	Tue Oct 28 11:05:44 2008 +0100
@@ -574,9 +574,6 @@
     let val thy = ProofContext.theory_of ctxt
         val th_cls_pairs = map (fn th => (Thm.get_name_hint th, ResAxioms.cnf_axiom thy th)) ths0
         val ths = List.concat (map #2 th_cls_pairs)
-        val _ = if exists(is_false o prop_of) cls 
-                then raise METIS "problem contains the empty clause"
-                else ();
         val _ = Output.debug (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
         val _ = app (fn th => Output.debug (fn () => Display.string_of_thm th)) cls
         val _ = Output.debug (fn () => "THEOREM CLAUSES")
@@ -593,6 +590,9 @@
                 else Output.debug (fn () => "goal is higher-order")
         val _ = Output.debug (fn () => "START METIS PROVE PROCESS")
     in
+        case List.filter (is_false o prop_of) cls of
+            false_th::_ => [false_th RS @{thm FalseE}]
+          | [] =>
         case refute thms of
             Metis.Resolution.Contradiction mth =>
               let val _ = Output.debug (fn () => "METIS RECONSTRUCTION START: " ^