# HG changeset patch
# User blanchet
# Date 1354789510 -3600
# Node ID 5c9a2f5ab3239893c5d9fc8d9646e14c85e94658
# Parent  c69a970143c0889b28436cdeaf015227c618e1df
more feature tweaks

diff -r c69a970143c0 -r 5c9a2f5ab323 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
@@ -462,8 +462,8 @@
 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 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 *))
@@ -573,8 +573,8 @@
 
 fun is_exists (s, _) = (s = @{const_name Ex} orelse s = @{const_name Ex1})
 
-val term_max_depth = 2
-val type_max_depth = 2
+val term_max_depth = 1
+val type_max_depth = 1
 
 (* TODO: Generate type classes for types? *)
 fun features_of ctxt prover thy (scope, status) ts =