src/Pure/Tools/named_thms.ML
changeset 30528 7173bf123335
parent 29579 cb520b766e00
child 31901 e280491f36b8
     1.1 --- a/src/Pure/Tools/named_thms.ML	Sun Mar 15 15:59:44 2009 +0100
     1.2 +++ b/src/Pure/Tools/named_thms.ML	Sun Mar 15 15:59:44 2009 +0100
     1.3 @@ -34,7 +34,7 @@
     1.4  val del = Thm.declaration_attribute del_thm;
     1.5  
     1.6  val setup =
     1.7 -  Attrib.add_attributes [(name, Attrib.add_del_args add del, "declaration of " ^ description)] #>
     1.8 +  Attrib.setup (Binding.name name) (Attrib.add_del add del) ("declaration of " ^ description) #>
     1.9    PureThy.add_thms_dynamic (Binding.name name, Data.get);
    1.10  
    1.11  end;