# HG changeset patch
# User blanchet
# Date 1388686056 -3600
# Node ID 25212efcd0de9a5816cf75df0f5dfdeb89ceea66
# Parent  7b18c41df27ab9b5438635129ea2396fcd63045f
removed pointless warning (cf. http://stackoverflow.com/questions/20233463/isabelle-metis-proof-state-contains-the-universal-sort/20785045#20785045)

diff -r 7b18c41df27a -r 25212efcd0de src/HOL/Tools/Metis/metis_tactic.ML
--- a/src/HOL/Tools/Metis/metis_tactic.ML	Thu Jan 02 09:50:22 2014 +0100
+++ b/src/HOL/Tools/Metis/metis_tactic.ML	Thu Jan 02 19:07:36 2014 +0100
@@ -13,7 +13,6 @@
   val verbose : bool Config.T
   val new_skolem : bool Config.T
   val advisory_simp : bool Config.T
-  val type_has_top_sort : typ -> bool
   val metis_tac : string list -> string -> Proof.context -> thm list -> int -> tactic
   val metis_lam_transs : string list
   val parse_metis_options : (string list option * string option) parser
@@ -250,9 +249,6 @@
    else
      all_tac) st0
 
-val type_has_top_sort =
-  exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false)
-
 fun generic_metis_tac type_encs lam_trans ctxt ths i st0 =
   let
     val _ = trace_msg ctxt (fn () =>
@@ -262,12 +258,7 @@
     fun tac clause =
       resolve_tac (FOL_SOLVE type_encs lam_trans ctxt clause ths) 1
   in
-    if exists_type type_has_top_sort (prop_of st0) then
-      verbose_warning ctxt "Proof state contains the universal sort {}"
-    else
-      ();
-    Meson.MESON (preskolem_tac ctxt)
-        (maps (neg_clausify ctxt (lam_trans = combsN))) tac ctxt i st0
+    Meson.MESON (preskolem_tac ctxt) (maps (neg_clausify ctxt (lam_trans = combsN))) tac ctxt i st0
   end
 
 fun metis_tac [] = generic_metis_tac partial_type_encs
diff -r 7b18c41df27a -r 25212efcd0de src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Thu Jan 02 09:50:22 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Thu Jan 02 19:07:36 2014 +0100
@@ -246,6 +246,9 @@
   | combine_interests _ Interesting = Interesting
   | combine_interests Boring Boring = Boring
 
+val type_has_top_sort =
+  exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false)
+
 fun is_likely_tautology_too_meta_or_too_technical th =
   let
     fun is_interesting_subterm (Const (s, _)) =