Anyway, the standard procedure for removal of old stuff is to start marking it as "old" or "legacy" in the NEWS, and emitting suitable legacy_warnings.
I will follow that standard procedure, once all occurrences of the old code generator invocations are replaced.
Put in legacy warnings already now, as they will alert users who accidentially type the wrong commands (remember our experience with the methods "evaluation" vs. "eval" last week). You don't have to wait with this until all else is resolved.
Alex _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
