src/Pure/Isar/theory_target.ML

   end;
 
 val type_syntax = target_decl Locale.add_type_syntax;
 val term_syntax = target_decl Locale.add_term_syntax;
 val declaration = target_decl Locale.add_declaration;
-
-fun target_naming (Target {target, ...}) lthy =
-  (if target = "" then Sign.naming_of (ProofContext.theory_of lthy)
-   else ProofContext.naming_of (LocalTheory.target_of lthy))
-  |> NameSpace.qualified_names;
 
 fun class_target (Target {target, ...}) f =
   LocalTheory.raw_theory f #>
   LocalTheory.target (Class.refresh_syntax target);
 

     define = define ta,
     notes = notes ta,
     type_syntax = type_syntax ta,
     term_syntax = term_syntax ta,
     declaration = declaration ta,
-    target_naming = target_naming ta,
     reinit = fn lthy => init_lthy_ctxt ta (ProofContext.theory_of lthy),
     exit = LocalTheory.target_of}
 and init_lthy_ctxt ta = init_lthy ta o init_ctxt ta;
 
 in