# HG changeset patch
# User blanchet
# Date 1354644614 -3600
# Node ID 4258aeca13a0838f9b2fc05dd495c80e249f4043
# Parent  db8cae658807768d14b902f0b9423cab578671e4
turned off noisy MaSh features

diff -r db8cae658807 -r 4258aeca13a0 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Tue Dec 04 19:09:44 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Tue Dec 04 19:10:14 2012 +0100
@@ -524,9 +524,11 @@
   thy_feature_name_of (Context.theory_name thy) ::
   interesting_terms_types_and_classes ctxt prover term_max_depth type_max_depth
                                       ts
-  |> forall is_lambda_free ts ? cons "no_lams"
-  |> forall (not o exists_Const is_exists) ts ? cons "no_skos"
+(* Temporarily disabled: These frequent features can easily dominate the others.
+  |> exists (not o is_lambda_free) ts ? cons "lams"
+  |> exists (exists_Const is_exists) ts ? cons "skos"
   |> scope <> Global ? cons "local"
+*)
   |> (case string_of_status status of "" => I | s => cons s)
 
 (* Too many dependencies is a sign that a crazy decision procedure is at work.