--- a/src/Pure/Isar/isar_syn.ML Wed May 12 15:23:38 2010 +0200
+++ b/src/Pure/Isar/isar_syn.ML Wed May 12 15:25:58 2010 +0200
@@ -181,7 +181,10 @@
val _ =
OuterSyntax.command "axioms" "state arbitrary propositions (axiomatic!)" K.thy_decl
- (Scan.repeat1 SpecParse.spec >> (Toplevel.theory o IsarCmd.add_axioms));
+ (Scan.repeat1 SpecParse.spec >>
+ (Toplevel.theory o
+ (IsarCmd.add_axioms o
+ tap (fn _ => legacy_feature "Old 'axioms' command -- use 'axiomatization' instead"))));
val opt_unchecked_overloaded =
Scan.optional (P.$$$ "(" |-- P.!!!