src/Pure/Isar/expression.ML

--- a/src/Pure/Isar/expression.ML	Fri Nov 13 19:57:46 2009 +0100
+++ b/src/Pure/Isar/expression.ML	Fri Nov 13 20:41:29 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 facts #> snd) notes';
+      |> fold (fn (kind, facts) => LocalTheory.notes_kind kind facts #> snd) notes';
 
   in (name, loc_ctxt) end;