src/HOL/Tools/Sledgehammer/metis_tactics.ML

                                     thms)
           in lmap |> fold (add_thm false) helper_ths end
   in (mode, add_type_thm (type_ext thy (map prop_of (cls @ ths))) lmap) end
 
 fun refute cls =
-    Metis.Resolution.loop (Metis.Resolution.new Metis.Resolution.default cls);
+    Metis.Resolution.loop (Metis.Resolution.new Metis.Resolution.default {axioms = cls, conjecture = []});
 
 fun is_false t = t aconv (HOLogic.mk_Trueprop HOLogic.false_const);
 
 fun common_thm ths1 ths2 = exists (member Thm.eq_thm ths1) (map Meson.make_meta_clause ths2);