--- a/src/Provers/clasimp.ML Sun Mar 15 15:59:44 2009 +0100
+++ b/src/Provers/clasimp.ML Sun Mar 15 15:59:44 2009 +0100
@@ -268,10 +268,10 @@
val iff_add' = attrib' addIffs_generic;
val iff_del = attrib (op delIffs) o attrib' delIffs_generic;
-val iff_att = Attrib.syntax (Scan.lift
+fun iff_att x = (Scan.lift
(Args.del >> K iff_del ||
Scan.option Args.add -- Args.query >> K iff_add' ||
- Scan.option Args.add >> K iff_add));
+ Scan.option Args.add >> K iff_add)) x;
(* method modifiers *)
@@ -311,8 +311,7 @@
(* theory setup *)
val clasimp_setup =
- (Attrib.add_attributes
- [("iff", iff_att, "declaration of Simplifier / Classical rules")] #>
+ (Attrib.setup @{binding iff} iff_att "declaration of Simplifier / Classical rules" #>
Method.add_methods
[("fastsimp", clasimp_method' fast_simp_tac, "combined fast and simp"),
("slowsimp", clasimp_method' slow_simp_tac, "combined slow and simp"),