src/HOL/Tools/Sledgehammer/metis_tactics.ML

     if exists_type type_has_topsort (prop_of st0) then
       (warning ("Metis: Proof state contains the universal sort {}"); Seq.empty)
     else
       (Meson.MESON (maps neg_clausify)
                    (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1)
-                   ctxt i
-       THEN Meson_Tactic.expand_defs_tac st0) st0
+                   ctxt i) st0
      handle ERROR msg => raise METIS ("generic_metis_tac", msg)
   end
   handle METIS (loc, msg) =>
          if mode = HO then
            (warning ("Metis: Falling back on \"metisFT\".");