# HG changeset patch
# User paulson
# Date 1199272958 -3600
# Node ID 466e714de2fcc70a1bb5fcf0e7fcfca8f698c7eb
# Parent  6d947d7a5ae81b38c928ab74552da9e2915a16bb
testing for empty sort

diff -r 6d947d7a5ae8 -r 466e714de2fc src/HOL/Tools/metis_tools.ML
--- 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;
diff -r 6d947d7a5ae8 -r 466e714de2fc src/HOL/Tools/res_atp.ML
--- a/src/HOL/Tools/res_atp.ML	Wed Jan 02 12:22:05 2008 +0100
+++ b/src/HOL/Tools/res_atp.ML	Wed Jan 02 12:22:38 2008 +0100
@@ -829,6 +829,8 @@
                       their original "name hints" may be bad anyway.*)
     val thy = ProofContext.theory_of ctxt
   in
+    if exists_type ResAxioms.type_has_empty_sort (prop_of goal)  
+    then error "Proof state contains the empty sort" else ();
     Output.debug (fn () => "subgoals in isar_atp:\n" ^
                   Syntax.string_of_term ctxt (Logic.mk_conjunction_list (Thm.prems_of goal)));
     Output.debug (fn () => "current theory: " ^ Context.theory_name thy);
diff -r 6d947d7a5ae8 -r 466e714de2fc src/HOL/Tools/res_axioms.ML
--- a/src/HOL/Tools/res_axioms.ML	Wed Jan 02 12:22:05 2008 +0100
+++ b/src/HOL/Tools/res_axioms.ML	Wed Jan 02 12:22:38 2008 +0100
@@ -11,6 +11,7 @@
   val pairname: thm -> string * thm
   val multi_base_blacklist: string list 
   val bad_for_atp: thm -> bool
+  val type_has_empty_sort: typ -> bool
   val cnf_rules_pairs: (string * thm) list -> (thm * (string * int)) list
   val cnf_rules_of_ths: thm list -> thm list
   val neg_clausify: thm list -> thm list
@@ -32,7 +33,11 @@
 (* FIXME legacy *)
 fun freeze_thm th = #1 (Drule.freeze_thaw th);
 
-
+fun type_has_empty_sort (TFree (_, [])) = true
+  | type_has_empty_sort (TVar (_, [])) = true
+  | type_has_empty_sort (Type (_, Ts)) = exists type_has_empty_sort Ts
+  | type_has_empty_sort _ = false;
+  
 (**** Transformation of Elimination Rules into First-Order Formulas****)
 
 val cfalse = cterm_of HOL.thy HOLogic.false_const;
@@ -343,7 +348,10 @@
     | _ => false;
 
 fun bad_for_atp th = 
-  PureThy.is_internal th orelse too_complex (prop_of th) orelse is_strange_thm th;
+  PureThy.is_internal th     
+  orelse too_complex (prop_of th)   
+  orelse exists_type type_has_empty_sort (prop_of th)  
+  orelse is_strange_thm th;
 
 val multi_base_blacklist =
   ["defs","select_defs","update_defs","induct","inducts","split","splits","split_asm",