--- 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);