1.1 --- a/src/Pure/codegen.ML	Sat Jul 23 23:33:59 2011 +0200
     1.2 +++ b/src/Pure/codegen.ML	Mon Jul 25 10:40:51 2011 +0200
     1.3 @@ -1012,6 +1012,7 @@
     1.4     || Scan.repeat1 (Parse.term >> pair "")) >>
     1.5    (fn ((((mode, module), opt_fname), modules), xs) => Toplevel.theory (fn thy =>
     1.6      let
     1.7 +      val _ = legacy_feature "Old code generation command -- use export_code instead";
     1.8        val mode' = (if lib then insert (op =) "library" else I) (remove (op =) "library" mode);
     1.9        val (code, gr) = generate_code thy mode' modules module xs;
    1.10        val thy' = thy |> Context.theory_map (ML_Context.exec (fn () =>