src/Pure/Isar/expression.ML
changeset 63402 f199837304d7
parent 63395 734723445a8c
child 66334 b210ae666a42
--- a/src/Pure/Isar/expression.ML	Tue Jul 05 23:39:49 2016 +0200
+++ b/src/Pure/Isar/expression.ML	Wed Jul 06 11:29:51 2016 +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 name
+      |> Named_Target.init NONE name
       |> fold (fn (kind, facts) => Local_Theory.notes_kind kind facts #> snd) notes';
 
   in (name, loc_ctxt) end;