# HG changeset patch
# User blanchet
# Date 1378763735 -7200
# Node ID 9770b0627de4c3714c9ba8ceb31bff8edea5ccc0
# Parent  c3d7d9911aae2786790792b500699f5cf7dfe1db
make facts like "mem_Collect_eq" more likely to be picked up by few-fact slices

diff -r c3d7d9911aae -r 9770b0627de4 src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Mon Sep 09 23:54:59 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Mon Sep 09 23:55:35 2013 +0200
@@ -387,7 +387,7 @@
 (* High enough so that it isn't wrongly considered as very relevant (e.g., for E
    weights), but low enough so that it is unlikely to be truncated away if few
    facts are included. *)
-val special_fact_index = 75
+val special_fact_index = 45
 
 fun relevance_filter ctxt thres0 decay max_facts is_built_in_const
         (fudge as {threshold_divisor, ridiculous_threshold, ...}) facts hyp_ts