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