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