# HG changeset patch
# User wenzelm
# Date 1198145779 -3600
# Node ID 31e7bd574eb9dca6a5ac26d7ecfe8309d0d903b6
# Parent  80c06e4d4db63459e36cdf1546ac01566983dc0a
made refute non-critical (seems to work after avoiding floating point random numbers);

diff -r 80c06e4d4db6 -r 31e7bd574eb9 src/HOL/Tools/metis_tools.ML
--- a/src/HOL/Tools/metis_tools.ML	Thu Dec 20 03:06:20 2007 +0100
+++ b/src/HOL/Tools/metis_tools.ML	Thu Dec 20 11:16:19 2007 +0100
@@ -557,8 +557,8 @@
         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);