src/Pure/General/position.ML

--- a/src/Pure/General/position.ML	Sat Dec 07 23:08:51 2024 +0100
+++ b/src/Pure/General/position.ML	Sat Dec 07 23:50:18 2024 +0100
@@ -54,8 +54,6 @@
   type report_text = report * string
   val reports_text: report_text list -> unit
   val reports: report list -> unit
-  val store_reports: report_text list Unsynchronized.ref ->
-    T list -> ('a -> Markup.T list) -> 'a -> unit
   val append_reports: report_text list Unsynchronized.ref -> report list -> unit
   val here_strs: T -> string * string
   val here: T -> string
@@ -271,11 +269,6 @@
 
 val reports = map (rpair "") #> reports_text;
 
-fun store_reports _ [] _ _ = ()
-  | store_reports (r: report_text list Unsynchronized.ref) ps markup x =
-      let val ms = markup x
-      in Unsynchronized.change r (fold (fn p => fold (fn m => cons ((p, m), "")) ms) ps) end;
-
 fun append_reports (r: report_text list Unsynchronized.ref) reports =
   Unsynchronized.change r (append (map (rpair "") reports));