# HG changeset patch
# User paulson
# Date 1260790213 0
# Node ID c907edcaab36ced3bfedd3305cfadda4bb0c0a7e
# Parent  ff8b2ac0134c30954117678ce0b79164fb793ed4
Upgraded a warning to an error

diff -r ff8b2ac0134c -r c907edcaab36 src/HOL/Tools/metis_tools.ML
--- 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