# HG changeset patch
# User blanchet
# Date 1284405789 -7200
# Node ID 7d850b17a7a6b1c1ad0cb09db3d7dc4f83a4e70d
# Parent  1e118007e41ac5e3c30f81b33a7b460c37c65c32
adapt to latest Metis version

diff -r 1e118007e41a -r 7d850b17a7a6 src/HOL/Tools/Sledgehammer/metis_tactics.ML
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Mon Sep 13 21:21:45 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Mon Sep 13 21:23:09 2010 +0200
@@ -735,7 +735,7 @@
   in (mode, 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);
+    Metis.Resolution.loop (Metis.Resolution.new Metis.Resolution.default {axioms = cls, conjecture = []});
 
 fun is_false t = t aconv (HOLogic.mk_Trueprop HOLogic.false_const);