src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML

       SOME (p_name, ind_T)
     else
       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)) =
         if (s, T) = ind_x orelse can dest_funT T then t else Var ((s, 0), T)
       | varify_noninducts t = t
     val p_inst =
       concl_prop |> map_aterms varify_noninducts |> close_form
                  |> 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
 
 fun type_match thy (T1, T2) =
   (Sign.typ_match thy (T2, T1) Vartab.empty; true)

 
 fun is_formula_type T = (T = HOLogic.boolT orelse T = propT)
 
 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
        prover, we introduce a fresh constant to simulate the effect of
        Skolemization. *)

       | (_, ts) => fold do_term ts
     fun do_quantifier will_surely_be_skolemized abs_T body_t =
       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 =
       if is_formula_type T then do_formula NONE else do_term
     and do_formula pos t =