# HG changeset patch
# User blanchet
# Date 1332157426 -3600
# Node ID 7e2c4da9ac7d169ab0591d6b34b1f286a000bbd4
# Parent  1d8601c642cce08a27783450ae8fb09d20da65c4
better defaults for Metis, that seem to make it less likely to loop seemingly forever -- 0 coefficients might very well make it incomplete

diff -r 1d8601c642cc -r 7e2c4da9ac7d src/HOL/Tools/Metis/metis_tactic.ML
--- a/src/HOL/Tools/Metis/metis_tactic.ML	Sun Mar 18 22:09:00 2012 +0100
+++ b/src/HOL/Tools/Metis/metis_tactic.ML	Mon Mar 19 12:43:46 2012 +0100
@@ -115,8 +115,8 @@
    postfactor = #postfactor Metis_Active.default}
 val waiting_params =
   {symbolsWeight = 1.0,
-   variablesWeight = 0.0,
-   literalsWeight = 0.0,
+   variablesWeight = 0.5,
+   literalsWeight = 0.1,
    models = []}
 val resolution_params = {active = active_params, waiting = waiting_params}