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;