# HG changeset patch
# User wenzelm
# Date 1267733425 -3600
# Node ID 8fbbfc39508ff56e3030a78459da9035fabebdc6
# Parent  309e75c58af2a1923d29f6a700f09e54357d2938
renamed type_has_empty_sort to type_has_topsort -- {} is the full universal sort;
metis: type_has_topsort leads to tactic failure (with warning), like other metis failures;

diff -r 309e75c58af2 -r 8fbbfc39508f src/HOL/Tools/metis_tools.ML
--- a/src/HOL/Tools/metis_tools.ML	Thu Mar 04 21:02:21 2010 +0100
+++ b/src/HOL/Tools/metis_tools.ML	Thu Mar 04 21:10:25 2010 +0100
@@ -714,12 +714,12 @@
   let val _ = trace_msg (fn () =>
         "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 (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
-        THEN Res_Axioms.expand_defs_tac st0) st0
+    if exists_type Res_Axioms.type_has_topsort (prop_of st0)
+    then raise METIS "Metis: Proof state contains the universal sort {}"
+    else
+      (Meson.MESON Res_Axioms.neg_clausify
+        (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1) ctxt i
+          THEN Res_Axioms.expand_defs_tac st0) st0
   end
   handle METIS s => (warning ("Metis: " ^ s); Seq.empty);
 
@@ -734,7 +734,7 @@
   type_lits_setup #>
   method @{binding metis} HO "METIS for FOL & HOL problems" #>
   method @{binding metisF} FO "METIS for FOL problems" #>
-  method @{binding metisFT} FT "METIS With-fully typed translation" #>
+  method @{binding metisFT} FT "METIS with fully-typed translation" #>
   Method.setup @{binding finish_clausify}
     (Scan.succeed (K (SIMPLE_METHOD (Res_Axioms.expand_defs_tac refl))))
     "cleanup after conversion to clauses";
diff -r 309e75c58af2 -r 8fbbfc39508f src/HOL/Tools/res_axioms.ML
--- a/src/HOL/Tools/res_axioms.ML	Thu Mar 04 21:02:21 2010 +0100
+++ b/src/HOL/Tools/res_axioms.ML	Thu Mar 04 21:10:25 2010 +0100
@@ -12,7 +12,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 type_has_topsort: typ -> bool
   val cnf_rules_pairs: theory -> (string * thm) list -> (thm * (string * int)) list
   val neg_clausify: thm list -> thm list
   val expand_defs_tac: thm -> tactic
@@ -31,10 +31,10 @@
 
 fun freeze_thm th = #1 (Drule.legacy_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;
+val type_has_topsort = Term.exists_subtype
+  (fn TFree (_, []) => true
+    | TVar (_, []) => true
+    | _ => false);
 
 
 (**** Transformation of Elimination Rules into First-Order Formulas****)
@@ -321,7 +321,7 @@
 
 fun bad_for_atp th =
   too_complex (prop_of th)
-  orelse exists_type type_has_empty_sort (prop_of th)
+  orelse exists_type type_has_topsort (prop_of th)
   orelse is_strange_thm th;
 
 val multi_base_blacklist =