# HG changeset patch
# User blanchet
# Date 1354789510 -3600
# Node ID 835a18063ed59612fd89684c2de21fa80731a6e4
# Parent  d8aa26c783279dd9073d9fd8c39c1401dcf45672
more MaSh feature tweaking

diff -r d8aa26c78327 -r 835a18063ed5 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Dec 06 11:25:10 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Dec 06 11:25:10 2012 +0100
@@ -459,12 +459,12 @@
             |> map snd |> take max_facts
     end
 
-fun thy_feature_of s = ("y" ^ s, 1.0 (* FUDGE *))
+fun thy_feature_of s = ("y" ^ s, 0.5 (* FUDGE *))
 fun const_feature_of s = ("c" ^ s, 1.0 (* FUDGE *))
 fun free_feature_of s = ("f" ^ s, 2.0 (* FUDGE *))
 fun type_feature_of s = ("t" ^ s, 1.0 (* FUDGE *))
 fun class_feature_of s = ("s" ^ s, 1.0 (* FUDGE *))
-fun status_feature_of status = (string_of_status status, 1.0 (* 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 *))