# HG changeset patch
# User wenzelm
# Date 1752571679 -7200
# Node ID c4b692b61e96141c9e8fc92ab72c1536c8b354f5
# Parent  a28bbeb76e22e516abd9a55a442a7919d464c5f5
clarified signature;

diff -r a28bbeb76e22 -r c4b692b61e96 src/Provers/clasimp.ML
--- a/src/Provers/clasimp.ML	Tue Jul 15 11:04:57 2025 +0200
+++ b/src/Provers/clasimp.ML	Tue Jul 15 11:27:59 2025 +0200
@@ -27,7 +27,7 @@
   val slow_simp_tac: Proof.context -> int -> tactic
   val best_simp_tac: Proof.context -> int -> tactic
   val iff_add: attribute
-  val iff_add': attribute
+  val iff_add_pure: attribute
   val iff_del: attribute
   val iff_modifiers: Method.modifier parser list
   val clasimp_modifiers: Method.modifier parser list
@@ -102,7 +102,7 @@
     Thm.attribute_declaration (iff_decl safe_atts unsafe_atts) th #>
     Thm.attribute_declaration Simplifier.simp_add th);
 
-val iff_add' = iff_decl pure_atts pure_atts;
+val iff_add_pure = iff_decl pure_atts pure_atts;
 
 val iff_del =
   Thm.declaration_attribute (fn th =>
@@ -188,7 +188,7 @@
     (Attrib.setup \<^binding>\<open>iff\<close>
       (Scan.lift
         (Args.del >> K iff_del ||
-          Scan.option Args.add -- Args.query >> K iff_add' ||
+          Scan.option Args.add -- Args.query >> K iff_add_pure ||
           Scan.option Args.add >> K iff_add))
       "declaration of Simplifier / Classical rules");
 
@@ -199,7 +199,7 @@
 
 val iff_modifiers =
  [Args.$$$ iffN -- Scan.option Args.add -- Args.colon >> K (Method.modifier iff_add \<^here>),
-  Args.$$$ iffN -- Scan.option Args.add -- Args.query_colon >> K (Method.modifier iff_add' \<^here>),
+  Args.$$$ iffN -- Scan.option Args.add -- Args.query_colon >> K (Method.modifier iff_add_pure \<^here>),
   Args.$$$ iffN -- Args.del -- Args.colon >> K (Method.modifier iff_del \<^here>)];
 
 val clasimp_modifiers =