src/HOL/Library/reify_data.ML
changeset 30528 7173bf123335
parent 29650 cc3958d31b1d
child 33518 24563731b9b2
     1.1 --- a/src/HOL/Library/reify_data.ML	Sun Mar 15 15:59:44 2009 +0100
     1.2 +++ b/src/HOL/Library/reify_data.ML	Sun Mar 15 15:59:44 2009 +0100
     1.3 @@ -32,8 +32,8 @@
     1.4  val radd = Thm.declaration_attribute (Data.map o apsnd o Thm.add_thm);
     1.5  val rdel = Thm.declaration_attribute (Data.map o apsnd o Thm.del_thm);
     1.6  
     1.7 -val setup = Attrib.add_attributes
     1.8 -  [("reify", Attrib.add_del_args add del, "Reify data"),
     1.9 -   ("reflection", Attrib.add_del_args radd rdel, "Reflection data")];
    1.10 +val setup =
    1.11 +  Attrib.setup @{binding reify} (Attrib.add_del add del) "reify data" #>
    1.12 +  Attrib.setup @{binding reflection} (Attrib.add_del radd rdel) "reflection data";
    1.13  
    1.14  end;