# HG changeset patch
# User wenzelm
# Date 1544784473 -3600
# Node ID e7fd8c6d183adf0c27581abcf20a54944076313f
# Parent  c8c3285f129414a868150233f642ff580b9b80c6
unused;

diff -r c8c3285f1294 -r e7fd8c6d183a src/Pure/General/input.ML
--- a/src/Pure/General/input.ML	Fri Dec 14 11:43:48 2018 +0100
+++ b/src/Pure/General/input.ML	Fri Dec 14 11:47:53 2018 +0100
@@ -19,7 +19,6 @@
   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;
 
@@ -64,9 +63,7 @@
 
 val source_content = source_content_range #> apsnd #1;
 
-val source_content_string = source_explode #> Symbol_Pos.content;
-
-val equal_content = (op =) o apply2 source_content_string;
+val equal_content = (op =) o apply2 (source_explode #> Symbol_Pos.content);
 
 end;