# HG changeset patch
# User blanchet
# Date 1355778388 -3600
# Node ID 4fff0898cc0e4befa53cd1be6f4d17c14016c1db
# Parent  681edd111e9b0de89af54c15dab84dc7ee18c296
tuned weights -- keep same relative values, but use 1.0 as the least weight

diff -r 681edd111e9b -r 4fff0898cc0e src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Dec 17 22:06:28 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Dec 17 22:06:28 2012 +0100
@@ -464,15 +464,15 @@
             |> map snd |> take max_facts
     end
 
-fun thy_feature_of s = ("y" ^ s, 0.5 (* FUDGE *))
-fun const_feature_of s = ("c" ^ s, 4.0 (* FUDGE *))
-fun free_feature_of s = ("f" ^ s, 5.0 (* FUDGE *))
-fun type_feature_of s = ("t" ^ s, 0.5 (* FUDGE *))
-fun class_feature_of s = ("s" ^ s, 0.25 (* FUDGE *))
-fun status_feature_of status = (string_of_status status, 0.5 (* FUDGE *))
-val local_feature = ("local", 2.0 (* FUDGE *))
-val lams_feature = ("lams", 0.5 (* FUDGE *))
-val skos_feature = ("skos", 0.5 (* FUDGE *))
+fun thy_feature_of s = ("y" ^ s, 2.0 (* FUDGE *))
+fun const_feature_of s = ("c" ^ s, 16.0 (* FUDGE *))
+fun free_feature_of s = ("f" ^ s, 20.0 (* FUDGE *))
+fun type_feature_of s = ("t" ^ s, 2.0 (* FUDGE *))
+fun class_feature_of s = ("s" ^ s, 1.0 (* FUDGE *))
+fun status_feature_of status = (string_of_status status, 2.0 (* FUDGE *))
+val local_feature = ("local", 8.0 (* FUDGE *))
+val lams_feature = ("lams", 2.0 (* FUDGE *))
+val skos_feature = ("skos", 2.0 (* FUDGE *))
 
 fun theory_ord p =
   if Theory.eq_thy p then