--- a/src/HOL/Tools/metis_tools.ML Mon Dec 14 11:01:04 2009 +0100
+++ b/src/HOL/Tools/metis_tools.ML Mon Dec 14 11:30:13 2009 +0000
@@ -715,7 +715,7 @@
"Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths))
in
if exists_type Res_Axioms.type_has_empty_sort (prop_of st0)
- then (warning "Proof state contains the empty sort"; Seq.empty)
+ then (error "metis: Proof state contains the empty sort"; Seq.empty)
else
(Meson.MESON Res_Axioms.neg_clausify
(fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1) ctxt i