diff -r 0fffc66b10d7 -r ac7570d80c3d src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Sat Mar 28 17:10:43 2009 +0100
+++ b/src/Pure/Isar/locale.ML	Sat Mar 28 17:21:11 2009 +0100
@@ -325,7 +325,7 @@
   | init_local_elem (Notes (kind, facts)) ctxt =
       let
         val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts
-      in ProofContext.note_thmss_i kind facts' ctxt |> snd end
+      in ProofContext.note_thmss kind facts' ctxt |> snd end
 
 fun cons_elem false (Notes notes) elems = elems
   | cons_elem _ elem elems = elem :: elems