changeset 30761 | ac7570d80c3d |
parent 30755 | 7ef503d216c2 |
child 30763 | 6976521b4263 |
--- 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