# HG changeset patch
# User wenzelm
# Date 1752570716 -7200
# Node ID df8de6dacede1a3496517670fba858a51a0ff289
# Parent  c4b692b61e96141c9e8fc92ab72c1536c8b354f5
tuned;

diff -r c4b692b61e96 -r df8de6dacede src/Provers/clasimp.ML
--- a/src/Provers/clasimp.ML	Tue Jul 15 11:27:59 2025 +0200
+++ b/src/Provers/clasimp.ML	Tue Jul 15 11:11:56 2025 +0200
@@ -195,12 +195,12 @@
 
 (* method modifiers *)
 
-val iffN = "iff";
+val iff_token = Args.$$$ "iff";
 
 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_pure \<^here>),
-  Args.$$$ iffN -- Args.del -- Args.colon >> K (Method.modifier iff_del \<^here>)];
+ [iff_token -- Scan.option Args.add -- Args.colon >> K (Method.modifier iff_add \<^here>),
+  iff_token -- Scan.option Args.add -- Args.query_colon >> K (Method.modifier iff_add_pure \<^here>),
+  iff_token -- Args.del -- Args.colon >> K (Method.modifier iff_del \<^here>)];
 
 val clasimp_modifiers =
   Simplifier.simp_modifiers @ Splitter.split_modifiers @