--- a/src/Pure/Isar/new_locale.ML Mon Dec 01 14:56:08 2008 +0100
+++ b/src/Pure/Isar/new_locale.ML Mon Dec 01 16:02:57 2008 +0100
@@ -295,7 +295,7 @@
| init_elem (Notes (kind, facts)) ctxt =
let
val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts
- in fold (fn args => Locale.local_note_qualified kind args #> snd) facts' ctxt end
+ in Locale.local_note_qualified kind facts' ctxt |> snd end
fun cons_elem false (Notes notes) elems = elems
| cons_elem _ elem elems = elem :: elems