src/Pure/ROOT.ML

--- a/src/Pure/ROOT.ML	Tue Dec 30 14:11:06 2014 +0100
+++ b/src/Pure/ROOT.ML	Tue Dec 30 23:45:03 2014 +0100
@@ -27,7 +27,6 @@
 use "General/properties.ML";
 use "General/output.ML";
 use "PIDE/markup.ML";
-fun legacy_feature s = warning (Markup.markup Markup.legacy ("Legacy feature! " ^ s));
 use "General/scan.ML";
 use "General/source.ML";
 use "General/symbol.ML";