src/Provers/clasimp.ML
changeset 58048 aa6296d09e0e
parent 58008 aa72531f972f
child 58826 2ed2eaabe3df
--- 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 @