# HG changeset patch
# User blanchet
# Date 1307571388 -7200
# Node ID f78d5f0818a0f8d738ce97dd7fe4e7291b150784
# Parent  82d4874757dfe61ce02cbcc20d1e4401bd924696
be a bit more liberal with respect to the universal sort -- it sometimes help

diff -r 82d4874757df -r f78d5f0818a0 src/HOL/Tools/Metis/metis_tactics.ML
--- a/src/HOL/Tools/Metis/metis_tactics.ML	Thu Jun 09 00:16:28 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_tactics.ML	Thu Jun 09 00:16:28 2011 +0200
@@ -207,10 +207,10 @@
     fun tac clause = resolve_tac (FOL_SOLVE type_syss 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 {}";
-       Seq.empty)
+      verbose_warning ctxt "Proof state contains the universal sort {}"
     else
-      Meson.MESON (preskolem_tac ctxt) (maps neg_clausify) tac ctxt i st0
+      ();
+    Meson.MESON (preskolem_tac ctxt) (maps neg_clausify) tac ctxt i st0
   end
 
 val metis_default_type_syss = [partial_type_sys, full_type_sys]