changeset 70545 | b93ba98e627a |
parent 70304 | 1514efa1e57a |
child 74112 | d0527bb2e590 |
--- a/src/Pure/Isar/attrib.ML Fri Aug 16 10:20:41 2019 +0200 +++ b/src/Pure/Isar/attrib.ML Fri Aug 16 10:33:25 2019 +0200 @@ -282,7 +282,7 @@ val atts = map (attribute_generic context) srcs; val (ths', context') = fold_map (curry (fold (uncurry o Thm.apply_attribute) atts)) ths context; - in (context', pick (name, Facts.pos_of_ref thmref) ths') end) + in (context', pick (name, Facts.ref_pos thmref) ths') end) end); in