--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Dec 05 22:04:01 2023 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Wed Dec 06 11:08:39 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))