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