# HG changeset patch
# User wenzelm
# Date 1198079527 -3600
# Node ID a7341f8ddf89c3552ff43ea1dda0856d39634b32
# Parent  0a599404f5a1e1b4d5a6ed97d87f102ca511d906
marked refute (the main metis procedure) as CRITICAL;

diff -r 0a599404f5a1 -r a7341f8ddf89 src/HOL/Tools/metis_tools.ML
--- 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);