# HG changeset patch # User wenzelm # Date 1723024681 -7200 # Node ID be3325cbeb40ae8d77c05e7771796459a5c0155c # Parent b98f1057da0edd342f4b2a9836cd14e64aff2a43 tuned: more antiquotations, avoid re-certification; diff -r b98f1057da0e -r be3325cbeb40 src/HOL/Tools/set_comprehension_pointfree.ML --- a/src/HOL/Tools/set_comprehension_pointfree.ML Tue Aug 06 22:47:44 2024 +0100 +++ b/src/HOL/Tools/set_comprehension_pointfree.ML Wed Aug 07 11:58:01 2024 +0200 @@ -461,21 +461,16 @@ |> Option.map (fn thm => thm RS @{thm eq_reflection}) end; -fun instantiate_arg_cong ctxt pred = - let - val arg_cong = Thm.incr_indexes (maxidx_of_term pred + 1) @{thm arg_cong} - val (Var (f, _) $ _, _) = HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.concl_of arg_cong)) - in - infer_instantiate ctxt [(f, Thm.cterm_of ctxt pred)] arg_cong - end; - fun proc ctxt redex = let - val pred $ set_compr = Thm.term_of redex - val arg_cong' = instantiate_arg_cong ctxt pred + val (f, set_compr) = Thm.dest_comb redex + val [A, B] = Thm.dest_ctyp (Thm.ctyp_of_cterm f) + val cong = + \<^instantiate>\'a = A and 'b = B and f + in lemma (schematic) "x = y \ f x \ f y" by simp\ in - conv ctxt set_compr - |> Option.map (fn thm => thm RS arg_cong' RS @{thm eq_reflection}) + conv ctxt (Thm.term_of set_compr) + |> Option.map (fn thm => thm RS cong) end; fun code_proc ctxt redex =