--- 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 =