# HG changeset patch
# User wenzelm
# Date 1723717359 -7200
# Node ID 043e5fd3ce328c968678c0de1db26b71f5f9e9ba
# Parent  82c0bfbaaa865a10aa490e2744a381ce96fd88bf
more direct access to Simplifier.mk_cong, to avoid odd Simpdata.mk_meta_cong seen in the wild;

diff -r 82c0bfbaaa86 -r 043e5fd3ce32 NEWS
--- a/NEWS	Thu Aug 15 11:49:45 2024 +0200
+++ b/NEWS	Thu Aug 15 12:22:39 2024 +0200
@@ -13,6 +13,9 @@
 'congproc' or 'weak_congproc' in the 'simproc_setup' command (or ML
 antiquotation of the same name).
 
+* The attribute "cong_format" produces the internal format of Simplifier
+"cong" rules, notably for congproc implementations.
+
 
 ** HOL **
 
diff -r 82c0bfbaaa86 -r 043e5fd3ce32 src/Pure/raw_simplifier.ML
--- a/src/Pure/raw_simplifier.ML	Thu Aug 15 11:49:45 2024 +0200
+++ b/src/Pure/raw_simplifier.ML	Thu Aug 15 12:22:39 2024 +0200
@@ -89,6 +89,7 @@
   val del_simp: thm -> Proof.context -> Proof.context
   val flip_simp: thm -> Proof.context -> Proof.context
   val init_simpset: thm list -> Proof.context -> Proof.context
+  val mk_cong: Proof.context -> thm -> thm
   val add_eqcong: thm -> Proof.context -> Proof.context
   val del_eqcong: thm -> Proof.context -> Proof.context
   val add_cong: thm -> Proof.context -> Proof.context
@@ -706,9 +707,9 @@
     is_full_cong_prems prems (xs ~~ ys)
   end;
 
-fun mk_cong ctxt = #mk_cong (get_mk_rews ctxt) ctxt;
+in
 
-in
+fun mk_cong ctxt = #mk_cong (get_mk_rews ctxt) ctxt;
 
 fun add_eqcong thm ctxt = ctxt |> map_simpset2
   (fn (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers) =>
diff -r 82c0bfbaaa86 -r 043e5fd3ce32 src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Thu Aug 15 11:49:45 2024 +0200
+++ b/src/Pure/simplifier.ML	Thu Aug 15 12:22:39 2024 +0200
@@ -59,6 +59,7 @@
   val add_simp: thm -> Proof.context -> Proof.context
   val del_simp: thm -> Proof.context -> Proof.context
   val init_simpset: thm list -> Proof.context -> Proof.context
+  val mk_cong: Proof.context -> thm -> thm
   val add_eqcong: thm -> Proof.context -> Proof.context
   val del_eqcong: thm -> Proof.context -> Proof.context
   val add_cong: thm -> Proof.context -> Proof.context
@@ -453,6 +454,8 @@
 
 (* setup attributes *)
 
+val cong_format = Scan.succeed (Thm.rule_attribute [] (Context.proof_of #> mk_cong));
+
 val _ = Theory.setup
  (Attrib.setup \<^binding>\<open>simp\<close> (Attrib.add_del simp_add simp_del)
     "declaration of Simplifier rewrite rule" #>
@@ -460,7 +463,8 @@
     "declaration of Simplifier congruence rule" #>
   Attrib.setup \<^binding>\<open>simproc\<close> simproc_att
     "declaration of simplification procedures" #>
-  Attrib.setup \<^binding>\<open>simplified\<close> simplified "simplified rule");
+  Attrib.setup \<^binding>\<open>simplified\<close> simplified "simplified rule" #>
+  Attrib.setup \<^binding>\<open>cong_format\<close> cong_format "internal format of Simplifier cong rule");