1.1 --- a/src/Pure/simplifier.ML	Sun Mar 15 15:59:44 2009 +0100
     1.2 +++ b/src/Pure/simplifier.ML	Sun Mar 15 15:59:44 2009 +0100
     1.3 @@ -334,11 +334,11 @@
     1.4  
     1.5  in
     1.6  
     1.7 -val simproc_att = Attrib.syntax
     1.8 -  (Scan.peek (fn context =>
     1.9 +val simproc_att =
    1.10 +  Scan.peek (fn context =>
    1.11      add_del :|-- (fn decl =>
    1.12        Scan.repeat1 (Args.named_attribute (decl o get_simproc context))
    1.13 -      >> (Library.apply o map Morphism.form))));
    1.14 +      >> (Library.apply o map Morphism.form)));
    1.15  
    1.16  end;
    1.17  
    1.18 @@ -355,10 +355,10 @@
    1.19  
    1.20  in
    1.21  
    1.22 -val simplified =
    1.23 -  Attrib.syntax (conv_mode -- Attrib.thms >> (fn (f, ths) => Thm.rule_attribute (fn context =>
    1.24 +val simplified = conv_mode -- Attrib.thms >>
    1.25 +  (fn (f, ths) => Thm.rule_attribute (fn context =>
    1.26      f ((if null ths then I else MetaSimplifier.clear_ss)
    1.27 -        (local_simpset_of (Context.proof_of context)) addsimps ths))));
    1.28 +        (local_simpset_of (Context.proof_of context)) addsimps ths)));
    1.29  
    1.30  end;
    1.31  
    1.32 @@ -366,11 +366,12 @@
    1.33  (* setup attributes *)
    1.34  
    1.35  val _ = Context.>> (Context.map_theory
    1.36 - (Attrib.add_attributes
    1.37 -   [(simpN, Attrib.add_del_args simp_add simp_del, "declaration of Simplifier rewrite rule"),
    1.38 -    (congN, Attrib.add_del_args cong_add cong_del, "declaration of Simplifier congruence rule"),
    1.39 -    ("simproc", simproc_att, "declaration of simplification procedures"),
    1.40 -    ("simplified", simplified, "simplified rule")]));
    1.41 + (Attrib.setup (Binding.name simpN) (Attrib.add_del simp_add simp_del)
    1.42 +    "declaration of Simplifier rewrite rule" #>
    1.43 +  Attrib.setup (Binding.name congN) (Attrib.add_del cong_add cong_del)
    1.44 +    "declaration of Simplifier congruence rule" #>
    1.45 +  Attrib.setup (Binding.name "simproc") simproc_att "declaration of simplification procedures" #>
    1.46 +  Attrib.setup (Binding.name "simplified") simplified "simplified rule"));
    1.47  
    1.48  
    1.49