src/Pure/Isar/isar_syn.ML

   OuterSyntax.local_theory "lemmas" "define lemmas" K.thy_decl (theorems Thm.lemmaK);
 
 val _ =
   OuterSyntax.local_theory "declare" "declare theorems (improper)" K.thy_decl
     (P.and_list1 SpecParse.xthms1
-      >> (fn args => #2 o Specification.theorems_cmd "" [((Name.no_binding, []), flat args)]));
+      >> (fn args => #2 o Specification.theorems_cmd "" [(Attrib.no_binding, flat args)]));
 
 
 (* name space entry path *)
 
 val _ =

 (* statements *)
 
 fun gen_theorem kind =
   OuterSyntax.local_theory_to_proof' kind ("state " ^ kind) K.thy_goal
     (Scan.optional (SpecParse.opt_thm_name ":" --|
-      Scan.ahead (SpecParse.locale_keyword || SpecParse.statement_keyword)) (Name.no_binding, []) --
+      Scan.ahead (SpecParse.locale_keyword || SpecParse.statement_keyword)) Attrib.no_binding --
       SpecParse.general_statement >> (fn (a, (elems, concl)) =>
         (Specification.theorem_cmd kind NONE (K I) a elems concl)));
 
 val _ = gen_theorem Thm.theoremK;
 val _ = gen_theorem Thm.lemmaK;