diff -r b3c45d0e4fe1 -r a8bcb5a446c8 src/Pure/ROOT
--- a/src/Pure/ROOT	Sat Nov 29 14:43:10 2014 +0100
+++ b/src/Pure/ROOT	Sun Nov 30 12:24:56 2014 +0100
@@ -81,6 +81,7 @@
     "General/graph.ML"
     "General/graph_display.ML"
     "General/heap.ML"
+    "General/input.ML"
     "General/integer.ML"
     "General/linear_set.ML"
     "General/long_name.ML"