better defaults for Metis, that seem to make it less likely to loop seemingly forever -- 0 coefficients might very well make it incomplete

--- 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}