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