1.1 --- a/src/Pure/Tools/named_thms.ML	Fri Oct 28 23:16:50 2011 +0200
     1.2 +++ b/src/Pure/Tools/named_thms.ML	Fri Oct 28 23:41:16 2011 +0200
     1.3 @@ -15,7 +15,7 @@
     1.4    val setup: theory -> theory
     1.5  end;
     1.6  
     1.7 -functor Named_Thms(val name: string val description: string): NAMED_THMS =
     1.8 +functor Named_Thms(val name: binding val description: string): NAMED_THMS =
     1.9  struct
    1.10  
    1.11  structure Data = Generic_Data
    1.12 @@ -38,7 +38,7 @@
    1.13  val del = Thm.declaration_attribute del_thm;
    1.14  
    1.15  val setup =
    1.16 -  Attrib.setup (Binding.name name) (Attrib.add_del add del) ("declaration of " ^ description) #>
    1.17 -  Global_Theory.add_thms_dynamic (Binding.name name, content);
    1.18 +  Attrib.setup name (Attrib.add_del add del) ("declaration of " ^ description) #>
    1.19 +  Global_Theory.add_thms_dynamic (name, content);
    1.20  
    1.21  end;