src/Pure/ROOT.ML
changeset 44549 5e5e6ad3922c
parent 44247 270366301bd7
child 44698 0385292321a0
     1.1 --- a/src/Pure/ROOT.ML	Sat Aug 27 16:22:59 2011 +0200
     1.2 +++ b/src/Pure/ROOT.ML	Sat Aug 27 17:26:14 2011 +0200
     1.3 @@ -31,6 +31,7 @@
     1.4  use "General/output.ML";
     1.5  use "General/timing.ML";
     1.6  use "General/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";