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