1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Tue Dec 04 22:14:59 2012 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Tue Dec 04 23:19:02 2012 +0100
     1.3 @@ -527,8 +527,11 @@
     1.4  (* Temporarily disabled: These frequent features can easily dominate the others.
     1.5    |> exists (not o is_lambda_free) ts ? cons "lams"
     1.6    |> exists (exists_Const is_exists) ts ? cons "skos"
     1.7 -  |> scope <> Global ? cons "local"
     1.8  *)
     1.9 +  |> scope <> Global
    1.10 +     (* temporary hack: give a heavier weight to locality *)
    1.11 +     ? append ["local0", "local1", "local2", "local3", "local4",
    1.12 +               "local5", "local6", "local7", "local8", "local9"]
    1.13    |> (case string_of_status status of "" => I | s => cons s)
    1.14  
    1.15  (* Too many dependencies is a sign that a crazy decision procedure is at work.