# HG changeset patch
# User blanchet
# Date 1292508737 -3600
# Node ID bf00e0a578e8ae01f78c18a9a60461a9f9d60482
# Parent  208bd47b6f29ef4deeb1dd27a65038cb588b4bb2
make it more likely that induction rules are picked up by Sledgehammer

diff -r 208bd47b6f29 -r bf00e0a578e8 src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Thu Dec 16 15:12:17 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Thu Dec 16 15:12:17 2010 +0100
@@ -167,7 +167,7 @@
       NONE
   | _ => NONE
 
-fun instantiate_induct_rule ctxt concl_prop p_name ((name, loc), (multi, th))
+fun instantiate_induct_rule ctxt concl_prop p_name ((name, _), (multi, th))
                             ind_x =
   let
     fun varify_noninducts (t as Free (s, T)) =
@@ -178,7 +178,8 @@
                  |> lambda (Free ind_x)
                  |> string_for_term ctxt
   in
-    ((fn () => name () ^ "[where " ^ p_name ^ " = " ^ quote p_inst ^ "]", loc),
+    ((fn () => name () ^ "[where " ^ p_name ^ " = " ^ quote p_inst ^ "]",
+      Local),
      (multi, th |> read_instantiate ctxt [((p_name, 0), p_inst)]))
   end
 
@@ -269,6 +270,13 @@
 
 fun pconsts_in_terms thy is_built_in_const also_skolems pos ts =
   let
+    (* Giving a penalty to Skolems is a good idea, but that penalty shouldn't
+       increase linearly with the number of Skolems in the fact. Hence, we
+       create equivalence classes of Skolems by reusing fresh Skolem names. *)
+    val skolem_cache = Unsynchronized.ref ""
+    fun get_skolem_name () =
+      (if !skolem_cache = "" then skolem_cache := gensym skolem_prefix else ();
+       !skolem_cache)
     val flip = Option.map not
     (* We include free variables, as well as constants, to handle locales. For
        each quantifiers that must necessarily be skolemized by the ATP, we
@@ -290,7 +298,7 @@
       do_formula pos body_t
       #> (if also_skolems andalso will_surely_be_skolemized then
             add_pconst_to_table true
-                (gensym skolem_prefix, PType (order_of_type abs_T, []))
+                (get_skolem_name (), PType (order_of_type abs_T, []))
           else
             I)
     and do_term_or_formula T =