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}