src/HOL/Tools/metis_tools.ML

                     else foldl (add_thm false ctxt) lmap (thEQ @ thS @ thC @ thB @ thK @ thI)
     in
         add_type_thm (type_ext thy (map prop_of (cls @ ths))) lmap'
     end;
 
-  fun refute cls = NAMED_CRITICAL "metis" (fn () =>
-      Metis.Resolution.loop (Metis.Resolution.new Metis.Resolution.default cls));
+  fun refute cls =
+      Metis.Resolution.loop (Metis.Resolution.new Metis.Resolution.default cls);
 
   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);