--- a/src/Pure/Syntax/term_position.ML Thu Oct 24 11:50:20 2024 +0200
+++ b/src/Pure/Syntax/term_position.ML Thu Oct 24 12:42:41 2024 +0200
@@ -1,7 +1,7 @@
(* Title: Pure/Syntax/term_position.ML
Author: Makarius
-Positions within term syntax trees (non-empty list).
+Reported positions within term syntax trees (non-empty list).
*)
signature TERM_POSITION =
@@ -44,9 +44,9 @@
val encode_none = YXML.string_of (encode_pos Position.none);
fun encode ps =
- (case remove (op =) Position.none ps of
+ (case filter Position.is_reported ps of
[] => encode_none
- | ps' => YXML.string_of_body (map encode_pos (distinct (op =) ps')));
+ | ps' => YXML.string_of_body (map encode_pos ps'));
val encode_prefix = YXML.XY ^ Markup.positionN;