# HG changeset patch
# User blanchet
# Date 1354659542 -3600
# Node ID 86cd7ee6f0c3d763098005f43f0a54e5c64b0253
# Parent  4a955d23c79b7f9b6d302ea87e3c25a43fee2ff6
promote local facts using a hack (for MaSh)

diff -r 4a955d23c79b -r 86cd7ee6f0c3 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Tue Dec 04 22:14:59 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Tue Dec 04 23:19:02 2012 +0100
@@ -527,8 +527,11 @@
 (* 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"
 *)
+  |> scope <> Global
+     (* temporary hack: give a heavier weight to locality *)
+     ? append ["local0", "local1", "local2", "local3", "local4",
+               "local5", "local6", "local7", "local8", "local9"]
   |> (case string_of_status status of "" => I | s => cons s)
 
 (* Too many dependencies is a sign that a crazy decision procedure is at work.