--- a/src/HOL/Tools/metis_tools.ML Wed Dec 19 16:32:16 2007 +0100
+++ b/src/HOL/Tools/metis_tools.ML Wed Dec 19 16:52:07 2007 +0100
@@ -557,8 +557,8 @@
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);
+ fun refute cls = NAMED_CRITICAL "metis" (fn () =>
+ Metis.Resolution.loop (Metis.Resolution.new Metis.Resolution.default cls));
fun is_false t = t aconv (HOLogic.mk_Trueprop HOLogic.false_const);