1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Dec 06 11:25:10 2012 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Dec 06 11:25:10 2012 +0100
     1.3 @@ -459,12 +459,12 @@
     1.4              |> map snd |> take max_facts
     1.5      end
     1.6  
     1.7 -fun thy_feature_of s = ("y" ^ s, 1.0 (* FUDGE *))
     1.8 +fun thy_feature_of s = ("y" ^ s, 0.5 (* FUDGE *))
     1.9  fun const_feature_of s = ("c" ^ s, 1.0 (* FUDGE *))
    1.10  fun free_feature_of s = ("f" ^ s, 2.0 (* FUDGE *))
    1.11  fun type_feature_of s = ("t" ^ s, 1.0 (* FUDGE *))
    1.12  fun class_feature_of s = ("s" ^ s, 1.0 (* FUDGE *))
    1.13 -fun status_feature_of status = (string_of_status status, 1.0 (* FUDGE *))
    1.14 +fun status_feature_of status = (string_of_status status, 0.5 (* FUDGE *))
    1.15  val local_feature = ("local", 2.0 (* FUDGE *))
    1.16  val lams_feature = ("lams", 0.5 (* FUDGE *))
    1.17  val skos_feature = ("skos", 0.5 (* FUDGE *))