src/Pure/Isar/attrib.ML
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