tuned signature;

--- a/src/Pure/General/input.ML	Mon Dec 10 20:35:08 2018 +0100
+++ b/src/Pure/General/input.ML	Mon Dec 10 22:38:03 2018 +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 source_content_string: 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 source_content_string = source_explode #> Symbol_Pos.content;
+
+val equal_content = (op =) o apply2 source_content_string;
 
 end;