--- a/src/Provers/clasimp.ML Wed Aug 27 12:32:42 2014 +0200
+++ b/src/Provers/clasimp.ML Wed Aug 27 14:54:32 2014 +0200
@@ -191,9 +191,9 @@
val iffN = "iff";
val iff_modifiers =
- [Args.$$$ iffN -- Scan.option Args.add -- Args.colon >> K ((I, iff_add): Method.modifier),
- Args.$$$ iffN -- Scan.option Args.add -- Args.query_colon >> K (I, iff_add'),
- Args.$$$ iffN -- Args.del -- Args.colon >> K (I, iff_del)];
+ [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 -- Args.del -- Args.colon >> K (Method.modifier iff_del @{here})];
val clasimp_modifiers =
Simplifier.simp_modifiers @ Splitter.split_modifiers @