Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
merged
authorblanchet
Mon, 14 Dec 2009 12:31:00 +0100
changeset 34122 9e6326db46b4
parent 34087 c907edcaab36 (diff)
parent 34121 5e831d805118 (current diff)
child 34123 c4988215a691
merged
--- a/src/HOL/Tools/metis_tools.ML	Mon Dec 14 12:30:26 2009 +0100
+++ b/src/HOL/Tools/metis_tools.ML	Mon Dec 14 12:31:00 2009 +0100
@@ -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
isabelle