# HG changeset patch # User blanchet # Date 1284618590 -7200 # Node ID 7e9879fbb7c56a3d6c4955e20e081b68fa5fadfc # Parent fbc1ab44b5f1f7f49eb40784b94a57870e099189 supply the Metis parameter defaults as argument, instead of patching the Metis sources; these values were found by Larry in 2007 and using anything else risks losing proofs diff -r fbc1ab44b5f1 -r 7e9879fbb7c5 src/HOL/Tools/Sledgehammer/metis_tactics.ML --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Thu Sep 16 08:27:10 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Thu Sep 16 08:29:50 2010 +0200 @@ -736,8 +736,24 @@ in lmap |> fold (add_thm false) helper_ths end in (mode, add_type_thm (type_ext thy (map prop_of (cls @ ths))) lmap) end +val clause_params = + {ordering = Metis_KnuthBendixOrder.default, + orderLiterals = Metis_Clause.UnsignedLiteralOrder, + orderTerms = true} +val active_params = + {clause = clause_params, + prefactor = #prefactor Metis_Active.default, + postfactor = #postfactor Metis_Active.default} +val waiting_params = + {symbolsWeight = 1.0, + variablesWeight = 0.0, + literalsWeight = 0.0, + models = []} +val refute_params = {active = active_params, waiting = waiting_params} + fun refute cls = - Metis_Resolution.loop (Metis_Resolution.new Metis_Resolution.default {axioms = cls, conjecture = []}); + Metis_Resolution.new refute_params {axioms = cls, conjecture = []} + |> Metis_Resolution.loop fun is_false t = t aconv (HOLogic.mk_Trueprop HOLogic.false_const);