src/Pure/General/input.ML

--- a/src/Pure/General/input.ML	Tue Mar 29 20:53:52 2016 +0200
+++ b/src/Pure/General/input.ML	Tue Mar 29 21:17:29 2016 +0200
@@ -15,6 +15,7 @@
   val string: string -> source
   val source_explode: source -> Symbol_Pos.T list
   val source_content: source -> string
+  val equal_content: source * source -> bool
 end;
 
 structure Input: INPUT =
@@ -38,6 +39,8 @@
 
 val source_content = source_explode #> Symbol_Pos.content;
 
+val equal_content = (op =) o apply2 source_content;
+
 end;
 
 end;