src/HOL/Import/shuffler.ML
changeset 30528 7173bf123335
parent 30510 4120fc59dd85
child 31241 b3c7044d47b6
--- a/src/HOL/Import/shuffler.ML	Sun Mar 15 15:59:44 2009 +0100
+++ b/src/HOL/Import/shuffler.ML	Sun Mar 15 15:59:44 2009 +0100
@@ -689,6 +689,6 @@
   add_shuffle_rule imp_comm #>
   add_shuffle_rule Drule.norm_hhf_eq #>
   add_shuffle_rule Drule.triv_forall_equality #>
-  Attrib.add_attributes [("shuffle_rule", Attrib.no_args shuffle_attr, "declare rule for shuffler")]
+  Attrib.setup @{binding shuffle_rule} (Scan.succeed shuffle_attr) "declare rule for shuffler";
 
 end