# HG changeset patch
# User blanchet
# Date 1292508737 -3600
# Node ID f9c7bdc75dd0819b8d7479431c3534dcc1d247f8
# Parent  b16fbb148a16b194bc5172da203732790cf0e4b9
reintroduce the higher penalty for skolems

diff -r b16fbb148a16 -r f9c7bdc75dd0 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
@@ -166,7 +166,7 @@
       NONE
   | _ => NONE
 
-fun instantiate_induct_rule ctxt concl_prop p_name ((name, _), (multi, th))
+fun instantiate_induct_rule ctxt concl_prop p_name ((name, loc), (multi, th))
                             ind_x =
   let
     fun varify_noninducts (t as Free (s, T)) =
@@ -177,8 +177,7 @@
                  |> lambda (Free ind_x)
                  |> string_for_term ctxt
   in
-    ((fn () => name () ^ "[where " ^ p_name ^ " = " ^ quote p_inst ^ "]",
-      Local),
+    ((fn () => name () ^ "[where " ^ p_name ^ " = " ^ quote p_inst ^ "]", loc),
      (multi, th |> read_instantiate ctxt [((p_name, 0), p_inst)]))
   end
 
@@ -261,13 +260,6 @@
 
 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 automatic
@@ -290,7 +282,7 @@
       do_formula pos body_t
       #> (if also_skolems andalso will_surely_be_skolemized then
             add_pconst_to_table true
-                (get_skolem_name (), PType (order_of_type abs_T, []))
+                (gensym skolem_prefix, PType (order_of_type abs_T, []))
           else
             I)
     and do_term_or_formula T =