--- 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
--- 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: " ^