src/Pure/General/input.ML

--- a/src/Pure/General/input.ML	Sun Dec 06 21:43:52 2020 +0100
+++ b/src/Pure/General/input.ML	Mon Dec 07 15:54:07 2020 +0100
@@ -19,6 +19,7 @@
   val source_explode: source -> Symbol_Pos.T list
   val source_content_range: source -> string * Position.range
   val source_content: source -> string * Position.T
+  val string_of: source -> string
   val equal_content: source * source -> bool
 end;
 
@@ -63,7 +64,9 @@
 
 val source_content = source_content_range #> apsnd #1;
 
-val equal_content = (op =) o apply2 (source_explode #> Symbol_Pos.content);
+val string_of = source_explode #> Symbol_Pos.content;
+
+val equal_content = (op =) o apply2 string_of;
 
 end;