diff -r 43a1f08c5a29 -r 4cdf7de81e1b src/HOL/Tools/metis_tools.ML
--- a/src/HOL/Tools/metis_tools.ML	Wed Dec 19 16:52:26 2007 +0100
+++ b/src/HOL/Tools/metis_tools.ML	Wed Dec 19 17:40:48 2007 +0100
@@ -586,7 +586,7 @@
                 else Output.debug (fn () => "goal is higher-order")
         val _ = Output.debug (fn () => "START METIS PROVE PROCESS")
     in
-        case refute thms of
+        case NAMED_CRITICAL "refute" (fn () => refute thms) of
             Metis.Resolution.Contradiction mth =>
               let val _ = Output.debug (fn () => "METIS RECONSTRUCTION START: " ^
                             Metis.Thm.toString mth)