# HG changeset patch
# User blanchet
# Date 1283184449 -7200
# Node ID f76ac80e9bcd4724eaf1e7d52e0bbfc8fd980eab
# Parent  a8aeaf9d4ca5ec74d5f2f645db9d84ca190ce37a
fiddle with fact filter

diff -r a8aeaf9d4ca5 -r f76ac80e9bcd src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Mon Aug 30 18:07:07 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Mon Aug 30 18:07:29 2010 +0200
@@ -142,7 +142,7 @@
 
 fun is_formula_type T = (T = HOLogic.boolT orelse T = propT)
 
-fun get_pconsts thy also_skolems pos ts =
+fun pconsts_in_terms thy also_skolems pos ts =
   let
     val flip = Option.map not
     (* We include free variables, as well as constants, to handle locales. For
@@ -282,7 +282,7 @@
 
 (* FUDGE *)
 val theory_bonus = Unsynchronized.ref 0.1
-val local_bonus = Unsynchronized.ref 0.2
+val local_bonus = Unsynchronized.ref 0.55
 val chained_bonus = Unsynchronized.ref 1.5
 
 fun locality_bonus General = 0.0
@@ -324,7 +324,7 @@
 
 fun pconsts_in_axiom thy t =
   Symtab.fold (fn (s, pss) => fold (cons o pair s) pss)
-              (get_pconsts thy true (SOME true) [t]) []
+              (pconsts_in_terms thy true (SOME true) [t]) []
 fun pair_consts_axiom theory_relevant thy axiom =
   case axiom |> snd |> theory_const_prop_of theory_relevant
              |> pconsts_in_axiom thy of
@@ -362,7 +362,7 @@
 
 fun if_empty_replace_with_locality thy axioms loc tab =
   if Symtab.is_empty tab then
-    get_pconsts thy false (SOME false)
+    pconsts_in_terms thy false (SOME false)
         (map_filter (fn ((_, loc'), th) =>
                         if loc' = loc then SOME (prop_of th) else NONE) axioms)
   else
@@ -379,7 +379,7 @@
     val const_tab =
       fold (count_axiom_consts theory_relevant thy) axioms Symtab.empty
     val goal_const_tab =
-      get_pconsts thy false (SOME false) goal_ts
+      pconsts_in_terms thy false (SOME false) goal_ts
       |> fold (if_empty_replace_with_locality thy axioms)
               [Chained, Local, Theory]
     val add_thms = maps (ProofContext.get_fact ctxt) add