merged

--- a/src/HOL/Tools/Metis/metis_tactic.ML	Mon Mar 19 15:19:38 2012 +0000
+++ b/src/HOL/Tools/Metis/metis_tactic.ML	Mon Mar 19 15:20:00 2012 +0000
@@ -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}