src/Pure/Isar/overloading.ML

           (fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts),
         abbrev = Generic_Target.abbrev
           (fn prmode => fn (b, mx) => fn (t, _) => fn _ =>
             Generic_Target.theory_abbrev prmode ((b, mx), t)),
         declaration = K Generic_Target.theory_declaration,
-        syntax_declaration = K Generic_Target.theory_declaration,
         pretty = pretty,
         exit = Local_Theory.target_of o conclude}
   end;
 
 val overloading = gen_overloading (fn ctxt => Syntax.check_term ctxt o Const);