# HG changeset patch
# User blanchet
# Date 1701863151 -3600
# Node ID 7529588b3daf8379179f3ce1da0d0ab2948ac1bc
# Parent  2413181b10bb21e8d17c72e7be74d89ec70feb4c# Parent  e6ae63d1b480a97920ac67bab9bf2a9a1e5eafca
merge

diff -r e6ae63d1b480 -r 7529588b3daf src/HOL/Tools/ATP/atp_problem_generate.ML
--- 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))
diff -r e6ae63d1b480 -r 7529588b3daf src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
--- 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"])] @
diff -r e6ae63d1b480 -r 7529588b3daf src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- 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