--- a/src/Pure/Isar/proof_context.ML Wed May 27 16:43:34 2020 +0200
+++ b/src/Pure/Isar/proof_context.ML Wed May 27 20:02:02 2020 +0200
@@ -979,9 +979,7 @@
| [] => err [] "Failed to retrieve literal fact"
| dups => err (distinct (op =) (map #2 dups)) "Ambiguous specification of literal fact");
- val markup =
- Markup.entity Markup.literal_factN ""
- |> Markup.properties (Position.def_properties_of thm_pos);
+ val markup = Position.entity_markup Markup.literal_factN ("", thm_pos);
val _ = Context_Position.report_generic context pos markup;
in pick true ("", thm_pos) [thm] end
| retrieve pick context (Facts.Named ((xname, pos), sel)) =