tuned;
authorwenzelm
Tue, 15 Jul 2025 11:11:56 +0200
changeset 82871 df8de6dacede
parent 82870 c4b692b61e96
child 82872 898d3860a204
tuned;
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 @