# HG changeset patch
# User blanchet
# Date 1354789510 -3600
# Node ID d2261e3141468c9f0edeb913c20d45724f949933
# Parent  b7b1f2a170b8da1918cd3adee0cee0a37c9d42ef
tweaked MaSh features, based on comments by Josef Urban

diff -r b7b1f2a170b8 -r d2261e314146 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
@@ -290,7 +290,7 @@
 
 local
 
-val version = "*** MaSh version 20121205b ***"
+val version = "*** MaSh version 20121205c ***"
 
 exception Too_New of unit
 
@@ -465,8 +465,8 @@
 fun class_feature_of s = ("s" ^ s, 1.0 (* FUDGE *))
 fun status_feature_of status = (string_of_status status, 1.0 (* FUDGE *))
 val local_feature = ("local", 2.0 (* FUDGE *))
-val lams_feature = ("lams", 1.0 (* FUDGE *))
-val skos_feature = ("skos", 1.0 (* FUDGE *))
+val lams_feature = ("lams", 0.5 (* FUDGE *))
+val skos_feature = ("skos", 0.5 (* FUDGE *))
 
 fun theory_ord p =
   if Theory.eq_thy p then