# HG changeset patch
# User wenzelm
# Date 1544477883 -3600
# Node ID 61396b9713d8b81761589d8155561205b7c815bb
# Parent  fc44536fa5059c07ee79572c679b5c7d26fd72a5
tuned signature;

diff -r fc44536fa505 -r 61396b9713d8 src/Pure/General/input.ML
--- 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;