src/HOL/Tools/metis_tools.ML
changeset 25761 466e714de2fc
parent 25724 31e7bd574eb9
child 26423 8408edac8f6b
--- a/src/HOL/Tools/metis_tools.ML	Wed Jan 02 12:22:05 2008 +0100
+++ b/src/HOL/Tools/metis_tools.ML	Wed Jan 02 12:22:38 2008 +0100
@@ -612,6 +612,8 @@
     let val _ = Output.debug (fn () =>
           "Metis called with theorems " ^ cat_lines (map string_of_thm ths))
     in
+       if exists_type ResAxioms.type_has_empty_sort (prop_of st0)  
+       then error "Proof state contains the empty sort" else ();
        (Meson.MESON ResAxioms.neg_clausify (fn cls => rtac (FOL_SOLVE mode ctxt cls ths) 1) i
         THEN ResAxioms.expand_defs_tac st0) st0
     end;