src/Pure/Isar/expression.ML

--- a/src/Pure/Isar/expression.ML	Fri Aug 04 08:12:37 2017 +0200
+++ b/src/Pure/Isar/expression.ML	Fri Aug 04 08:12:37 2017 +0200
@@ -825,7 +825,7 @@
     val loc_ctxt = thy'
       |> Locale.register_locale binding (extraTs, params)
           (asm, rev defs) (a_intro, b_intro) axioms hyp_spec [] (rev notes) (rev deps')
-      |> Named_Target.init NONE name
+      |> Named_Target.init name
       |> fold (fn (kind, facts) => Local_Theory.notes_kind kind facts #> snd) notes';
 
   in (name, loc_ctxt) end;