1.1 --- a/src/HOL/Tools/Metis/metis_tactics.ML	Thu Jun 09 00:16:28 2011 +0200
     1.2 +++ b/src/HOL/Tools/Metis/metis_tactics.ML	Thu Jun 09 00:16:28 2011 +0200
     1.3 @@ -207,10 +207,10 @@
     1.4      fun tac clause = resolve_tac (FOL_SOLVE type_syss ctxt clause ths) 1
     1.5    in
     1.6      if exists_type type_has_top_sort (prop_of st0) then
     1.7 -      (verbose_warning ctxt "Proof state contains the universal sort {}";
     1.8 -       Seq.empty)
     1.9 +      verbose_warning ctxt "Proof state contains the universal sort {}"
    1.10      else
    1.11 -      Meson.MESON (preskolem_tac ctxt) (maps neg_clausify) tac ctxt i st0
    1.12 +      ();
    1.13 +    Meson.MESON (preskolem_tac ctxt) (maps neg_clausify) tac ctxt i st0
    1.14    end
    1.15  
    1.16  val metis_default_type_syss = [partial_type_sys, full_type_sys]