# HG changeset patch
# User blanchet
# Date 1332247989 -3600
# Node ID 10bece4ac87ea8153ebcbef61737106647f5b5cd
# Parent  62ca06cc5a999d44116ccbe3ebeaf3a9e841cff6
more conservative Metis defaults, for backward compatiblity (as illustrated by one "metis" call in "Auth/KerberosV")

diff -r 62ca06cc5a99 -r 10bece4ac87e src/HOL/Tools/Metis/metis_tactic.ML
--- a/src/HOL/Tools/Metis/metis_tactic.ML	Tue Mar 20 13:53:09 2012 +0100
+++ b/src/HOL/Tools/Metis/metis_tactic.ML	Tue Mar 20 13:53:09 2012 +0100
@@ -118,8 +118,8 @@
    postfactor = #postfactor Metis_Active.default}
 val waiting_params =
   {symbolsWeight = 1.0,
-   variablesWeight = 0.5,
-   literalsWeight = 0.1,
+   variablesWeight = 0.05,
+   literalsWeight = 0.01,
    models = []}
 fun resolution_params ordering =
   {active = active_params ordering, waiting = waiting_params}