src/Pure/Isar/expression.ML

     val axioms = map Element.conclude_witness b_axioms;
 
     val loc_ctxt = thy'
       |> Locale.register_locale binding (extraTs, params)
           (asm, rev defs) (a_intro, b_intro) axioms [] (rev notes) (rev deps')
-      |> Theory_Target.init (SOME name)
+      |> Named_Target.init (SOME name)
       |> fold (fn (kind, facts) => Local_Theory.notes_kind kind facts #> snd) notes';
 
   in (name, loc_ctxt) end;
 
 in

 local
 
 fun gen_sublocale prep_expr intern raw_target expression thy =
   let
     val target = intern thy raw_target;
-    val target_ctxt = Theory_Target.init (SOME target) thy;
+    val target_ctxt = Named_Target.init (SOME target) thy;
     val ((propss, deps, export), goal_ctxt) = prep_expr expression target_ctxt;
     fun after_qed witss = ProofContext.theory
       (fold (fn ((dep, morph), wits) => Locale.add_dependency
         target (dep, morph $> Element.satisfy_morphism wits) export) (deps ~~ witss));
   in Element.witness_proof after_qed propss goal_ctxt end;