Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/metis_tools.ML
changeset 25710 4cdf7de81e1b
parent 25708 a7341f8ddf89
child 25713 1c45623e0edf 
--- 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)
isabelle