changeset 33671 | 4b0f2599ed48 |
parent 33670 | 02b7738aef6a |
child 35021 | c839a4c670c6 |
--- a/src/Pure/Isar/expression.ML Fri Nov 13 20:41:29 2009 +0100 +++ b/src/Pure/Isar/expression.ML Fri Nov 13 21:11:15 2009 +0100 @@ -775,7 +775,7 @@ |> Locale.register_locale binding (extraTs, params) (asm, rev defs) (a_intro, b_intro) axioms ([], []) (rev notes) (rev deps') |> Theory_Target.init (SOME name) - |> fold (fn (kind, facts) => LocalTheory.notes_kind kind facts #> snd) notes'; + |> fold (fn (kind, facts) => Local_Theory.notes_kind kind facts #> snd) notes'; in (name, loc_ctxt) end;