src/Pure/ROOT.ML
changeset 59203 5f0bd5afc16d
parent 59196 73a6403637b3
child 59363 4660b0409096
     1.1 --- a/src/Pure/ROOT.ML	Tue Dec 30 14:11:06 2014 +0100
     1.2 +++ b/src/Pure/ROOT.ML	Tue Dec 30 23:45:03 2014 +0100
     1.3 @@ -27,7 +27,6 @@
     1.4  use "General/properties.ML";
     1.5  use "General/output.ML";
     1.6  use "PIDE/markup.ML";
     1.7 -fun legacy_feature s = warning (Markup.markup Markup.legacy ("Legacy feature! " ^ s));
     1.8  use "General/scan.ML";
     1.9  use "General/source.ML";
    1.10  use "General/symbol.ML";