src/Pure/Isar/proof_context.ML

           (case distinct (eq_fst Thm.eq_thm_prop) results of
             [res] => res
           | [] => 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)) =
       let
         val thy = Context.theory_of context;