--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Wed Dec 06 12:06:29 2023 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Wed Dec 06 12:45:51 2023 +0100
@@ -1428,23 +1428,6 @@
((lam_fact_prefix ^ Int.toString (j + 1), (Global, Non_Rec_Def)), (Axiom, t)))
in (facts, lam_facts) end
-(* Metis's use of "resolve_tac" freezes the schematic variables. We simulate this in Sledgehammer to
- prevent the discovery of unreplayable proofs. *)
-fun freeze_term t =
- let
- (* Freshness is desirable for completeness, but not for soundness. *)
- fun indexed_name (s, i) = s ^ "_" ^ string_of_int i ^ atp_weak_suffix
- fun freeze (t $ u) = freeze t $ freeze u
- | freeze (Abs (s, T, t)) = Abs (s, T, freeze t)
- | freeze (Var (x, T)) = Free (indexed_name x, T)
- | freeze t = t
- fun freeze_tvar (x, S) = TFree (indexed_name x, S)
- in
- t |> exists_subterm is_Var t ? freeze
- |> exists_type (exists_subtype is_TVar) t
- ? map_types (map_type_tvar freeze_tvar)
- end
-
fun presimp_prop simp_options ctxt type_enc t =
let
val t =
@@ -2080,8 +2063,6 @@
performance (for some reason). *)
val hyp_ts = hyp_ts |> map (fn t => if member (op aconv) fact_ts t then \<^prop>\<open>True\<close> else t)
- val hyp_ts = map freeze_term hyp_ts;
- val concl_t = freeze_term concl_t;
val maybe_presimp_prop = presimp ? presimp_prop simp_options ctxt type_enc
val facts = facts |> map (apsnd (pair Axiom o maybe_presimp_prop))
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Wed Dec 06 12:06:29 2023 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Wed Dec 06 12:45:51 2023 +0100
@@ -293,23 +293,7 @@
fun hammer_away override_params writeln_result subcommand opt_i fact_override state0 =
let
- (* We generally want chained facts to be picked up by the relevance filter, because it can then
- give it a proper name, which is useful for a variety of reasons (minimization, Isar proofs,
- verbose output, machine learning). However, if the fact is available by no other means (not
- even backticks), as "f" would be in "using f unfolding f'" after unfolding, we have no choice
- but to insert it into the state as an additional hypothesis. *)
- val {facts = chained0, ...} = Proof.goal state0
- val (inserts, keep_chained) =
- if null chained0 orelse #only fact_override then
- (chained0, [])
- else
- let val ctxt0 = Proof.context_of state0 in
- List.partition (is_useful_unnamed_local_fact ctxt0) chained0
- end
- val state = state0
- |> (if null inserts then I else Proof.refine_insert inserts #> Proof.set_facts keep_chained)
- |> silence_state
-
+ val state = silence_state state0
val thy = Proof.theory_of state
val ctxt = Proof.context_of state
@@ -329,7 +313,7 @@
(if subcommand = relearn_isarN orelse subcommand = relearn_proverN then mash_unlearn ctxt
else ();
mash_learn ctxt
- (* TODO: Use MaSh mode instead and have the special defaults hardcoded in "get_params" *)
+ (* TODO: Use MaSh mode instead and have the special defaults hardcoded in "get_params". *)
(get_params Normal thy
([("timeout", [string_of_real default_learn_prover_timeout]),
("slice", ["false"])] @
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Wed Dec 06 12:06:29 2023 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Wed Dec 06 12:45:51 2023 +0100
@@ -32,7 +32,6 @@
val instantiate_inducts : Proof.context -> term list -> term ->
(((unit -> string) * 'a) * thm) list -> (((unit -> string) * 'a) * thm) list
val fact_of_lazy_fact : lazy_fact -> fact
- val is_useful_unnamed_local_fact : Proof.context -> thm -> bool
val all_facts : Proof.context -> bool -> Keyword.keywords -> thm list -> thm list ->
status Termtab.table -> lazy_fact list